Fermat's Last Theorem

The theorem asserts: for every natural number $n$ with $3 \le n$, and for all natural numbers $a, b, c$ with $0 < a$, $0 < b$ and $0 < c$, one has $a^n + b^n \neq c^n$. Every quantity occurring is a natural number; the arithmetic is the arithmetic of $\mathbb{N}$, so the equation is the unsigned one and no rearrangement with signs is involved. The three positivity hypotheses are stated separately, one for each of $a$, $b$, $c$; they exclude exactly the degenerate identities $0^n + b^n = b^n$ and $a^n + 0^n = a^n$ (and, with $c = 0$, the impossible $a^n + b^n = 0$). The hypothesis $3 \le n$ restricts the exponent: nothing is claimed for $n \le 2$; indeed for $n = 1, 2$ the conclusion fails, since $1^1 + 1^1 = 2^1$ and $3^2 + 4^2 = 5^2$. The conclusion is a negation of an equality of natural numbers, quantified over all admissible $n, a, b, c$ simultaneously; it is the elementary, fully unfolded form of Fermat's assertion, using no project-specific notion and only Mathlib's natural numbers and their power operation.

This is Fermat's Last Theorem in its elementary spelling, the statement proved by Wiles, with Taylor–Wiles, completing the chain through Frey, Serre and Ribet. Mathlib's own formulation is the predicate FermatLastTheorem, namely $\forall n \ge 3$, $\forall a, b, c$ nonzero natural numbers, $a^n + b^n \neq c^n$; that version phrases the nondegeneracy as $a \neq 0$ rather than $0 < a$, and the two formulations are interderivable in one step each way. Being the top-level assertion, it is not used as an input anywhere else in the development.