Statement of Fermat's Last Theorem

This file states Fermat's Last Theorem. We provide a statement over a general semiring with specific exponent, along with the usual statement over the naturals.

def FermatLastTheoremWith (α : Type u_1) [Semiring α] (n : ℕ) : Prop

Statement of Fermat's Last Theorem over a given semiring with a specific exponent.

Equations

• FermatLastTheoremWith α n = ∀ (a b c : α), a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

def FermatLastTheoremFor (n : ℕ) : Prop

Statement of Fermat's Last Theorem over the naturals for a given exponent.

Equations

• FermatLastTheoremFor n = FermatLastTheoremWith ℕ n

def FermatLastTheorem : Prop

Statement of Fermat's Last Theorem: a ^ n + b ^ n = c ^ n has no nontrivial natural solution when n ≥ 3.

Equations

• FermatLastTheorem = ∀ n ≥ 3, FermatLastTheoremFor n

theorem fermatLastTheoremFor_zero : FermatLastTheoremFor 0

theorem not_fermatLastTheoremFor_one : ¬FermatLastTheoremFor 1

theorem not_fermatLastTheoremFor_two : ¬FermatLastTheoremFor 2

theorem FermatLastTheoremWith.mono {α : Type u_1} [Semiring α] [NoZeroDivisors α] {m : ℕ} {n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremWith α m) : FermatLastTheoremWith α n

theorem FermatLastTheoremFor.mono {m : ℕ} {n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremFor m) : FermatLastTheoremFor n

theorem fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

theorem fermatLastTheoremFor_iff_nat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n

theorem fermatLastTheoremFor_iff_int {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n

theorem fermatLastTheoremFor_iff_rat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n

theorem fermatLastTheoremWith_of_fermatLastTheoremWith_coprime {n : ℕ} {R : Type u_2} [CommSemiring R] [IsDomain R] [DecidableEq R] [NormalizedGCDMonoid R] (hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith R n

To prove Fermat Last Theorem in any semiring that is a NormalizedGCDMonoid one can assume that the gcd of {a, b, c} is 1.

theorem dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT {n : ℕ} {p : ℤ} (hp : Prime p) {a : ℤ} {b : ℤ} {c : ℤ} (hpa : p ∣ a) (hpb : p ∣ b) (HF : a ^ n + b ^ n + c ^ n = 0) : p ∣ c

theorem isCoprime_of_gcd_eq_one_of_FLT {n : ℕ} {a : ℤ} {b : ℤ} {c : ℤ} (Hgcd : {a, b, c}.gcd id = 1) (HF : a ^ n + b ^ n + c ^ n = 0) : IsCoprime a b