Rarely you can find a proof that assumes the axiom of choice in such an obvious way.
This proof is non-constructive because proof-by-contradiction proofs that can't be changed into proof-by-negation proofs are not allowed in constructive math, because there's no law of excluded middle with infinite sets in constructive math, which follows from a lack of a strong axiom of choice.
This proof says that the set of prime numbers can't be finite. Only in classical logic you can deduce from this that the set of prime numbers must be infinite. In intuitionistic logic you can't deduce this.
This is interesting because most "normal" proofs and results can be written so that they are valid both in classical logic and intuitionistic logic. Only "crazy" results like the Banach–Tarski theorem are different.
An yet this is a trivial proof of a trivial result that can't be easily converted to constructivism. That is why it screams of axiom of choice.
? I was not aware of any system where proof by contradiction isn't acceptable.
The opposite of false is true.
But apparently you are right. https://en.wikipedia.org/wiki/Intuitionistic_logic
> intuitionistic logic has no interpretation as a two-valued logic