The irrationality of $\sqrt[n]{2}$ from the FLT.

Question

It's common to see the Fermat Last Theorem being used to prove the irrationality of $\sqrt[n]{2}$. In fact, according this post, the said proof appeared in American Mathematical Monthly.

On the other hand, I have seen two objections on this approach: DanielLittlewood's comment here and BCnrd's comment here.

Since I'm not able to judge by myself, I'd like a definitive answer: Is this proof logically valid?

Edit

It seems the phrase "logically valid" is not appropriate for the context. In fact, I want to know if the proof is circular (as suggested in the linked comments).

Answer 1

The proof is logically valid. Even if Wiles' proof depends on $\sqrt[n] 2$ being irrational, this does not make the proof circular - just redundant. The reason is, the irrationality of $\sqrt[n] 2$ can be easily proven without resorting to Fermat's last theorem. Thus Wiles' proof would still hold without this proof of the irrationality of $\sqrt[n] 2$.

Concerning BCnrd's comment, it only points out that the irrationality of $\sqrt[n] 2$ is easily proven on the way to proving FLT.

Answer 2

It is a logically valid proof. BCnrd's comment describes it as "circular", but I guess what he really means is something like "redundant". A proof is a sequence of formulas each of which is a direct consequence of formulas appearing earlier in the sequence, and the theorem it proves (its conclusion) is the last formula in the sequence. Essentially we are talking about a proof that first includes a formula $A$ meaning $\sqrt[n] 2$ is irrational for $n \gt 1$, then later has a formula $B$ expressing FLT (perhaps depending on $A$), then proves $B \rightarrow A$, and finally concludes with $A$ by modus ponens. It is still a valid proof of $A$ even though $A$ appears multiple times and the proof could have concluded at any of those earlier times.