The reduction of FLT to the p>=5 prime case.

theorem Nat.three_dvd_or_four_dvd_or_prime_dvd {n : ℕ} (hn : 3 ≤ n) : 3 ∣ n ∨ 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ 5 ≤ p ∧ p ∣ n

theorem FermatLastTheorem.of_p_ge_5 (H : ∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p) : FermatLastTheorem

If Fermat's Last Theorem is true for primes p ≥ 5, then FLT is true.

theorem PNat.pow_add_pow_ne_pow_of_FermatLastTheorem : FermatLastTheorem → ∀ (a b c : ℕ+), ∀ n > 2, a ^ n + b ^ n ≠ c ^ n

Fermat's Last Theorem as stated in mathlib (a statement FermatLastTheorem about naturals) implies Fermat's Last Theorem stated in terms of positive integers.