English
To prove Fermat's Last Theorem for all n, it suffices to prove it for odd prime exponents.
Русский
Достаточно доказать Ферма для всех нечетных простых экспонент, чтобы вывести общий случай.
LaTeX
$$$\text{FLT}(n)\Leftarrow n\in\mathbb{N},\; n\ge 3 \text{ odd prime} \Rightarrow \text{FLT}(n)$$$
Lean4
/-- To prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.
-/
theorem of_odd_primes (hprimes : ∀ p : ℕ, Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem :=
by
intro n h
obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h <;>
apply FermatLastTheoremWith.mono hdvd
· exact fermatLastTheoremFour
· exact hprimes p hpprime hpodd
