Fermat's Last Theorem for the case n = 4

There are no non-zero integers a, b and c such that a ^ 4 + b ^ 4 = c ^ 4.

def Fermat42 (a b c : Int) : Prop

Shorthand for three non-zero integers a, b, and c satisfying a ^ 4 + b ^ 4 = c ^ 2. We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4 follows.

Equations

• Eq (Fermat42 a b c) (And (Ne a 0) (And (Ne b 0) (Eq (HAdd.hAdd (HPow.hPow a 4) (HPow.hPow b 4)) (HPow.hPow c 2))))

theorem Fermat42.comm {a b c : Int} : Iff (Fermat42 a b c) (Fermat42 b a c)

theorem Fermat42.mul {a b c k : Int} (hk0 : Ne k 0) : Iff (Fermat42 a b c) (Fermat42 (HMul.hMul k a) (HMul.hMul k b) (HMul.hMul (HPow.hPow k 2) c))

theorem Fermat42.ne_zero {a b c : Int} (h : Fermat42 a b c) : Ne c 0

def Fermat42.Minimal (a b c : Int) : Prop

We say a solution to a ^ 4 + b ^ 4 = c ^ 2 is minimal if there is no other solution with a smaller c (in absolute value).

Equations

• Eq (Fermat42.Minimal a b c) (And (Fermat42 a b c) (∀ (a1 b1 c1 : Int), Fermat42 a1 b1 c1 → LE.le c.natAbs c1.natAbs))

theorem Fermat42.exists_minimal {a b c : Int} (h : Fermat42 a b c) : Exists fun (a0 : Int) => Exists fun (b0 : Int) => Exists fun (c0 : Int) => Minimal a0 b0 c0

if we have a solution to a ^ 4 + b ^ 4 = c ^ 2 then there must be a minimal one.

theorem Fermat42.coprime_of_minimal {a b c : Int} (h : Minimal a b c) : IsCoprime a b

a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 must have a and b coprime.

theorem Fermat42.minimal_comm {a b c : Int} : Minimal a b c → Minimal b a c

We can swap a and b in a minimal solution to a ^ 4 + b ^ 4 = c ^ 2.

theorem Fermat42.neg_of_minimal {a b c : Int} : Minimal a b c → Minimal a b (Neg.neg c)

We can assume that a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 has positive c.

theorem Fermat42.exists_odd_minimal {a b c : Int} (h : Fermat42 a b c) : Exists fun (a0 : Int) => Exists fun (b0 : Int) => Exists fun (c0 : Int) => And (Minimal a0 b0 c0) (Eq (HMod.hMod a0 2) 1)

We can assume that a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 has a odd.

theorem Fermat42.exists_pos_odd_minimal {a b c : Int} (h : Fermat42 a b c) : Exists fun (a0 : Int) => Exists fun (b0 : Int) => Exists fun (c0 : Int) => And (Minimal a0 b0 c0) (And (Eq (HMod.hMod a0 2) 1) (LT.lt 0 c0))

We can assume that a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 has a odd and c positive.

theorem Int.isCoprime_of_sq_sum {r s : Int} (h2 : IsCoprime s r) : IsCoprime (HAdd.hAdd (HPow.hPow r 2) (HPow.hPow s 2)) r

@[deprecated Int.isCoprime_of_sq_sum (since := "2025-01-23")]

theorem Int.coprime_of_sq_sum {r s : Int} (h2 : IsCoprime s r) : IsCoprime (HAdd.hAdd (HPow.hPow r 2) (HPow.hPow s 2)) r

Alias of Int.isCoprime_of_sq_sum.

theorem Int.isCoprime_of_sq_sum' {r s : Int} (h : IsCoprime r s) : IsCoprime (HAdd.hAdd (HPow.hPow r 2) (HPow.hPow s 2)) (HMul.hMul r s)

@[deprecated Int.isCoprime_of_sq_sum' (since := "2025-01-23")]

theorem Int.coprime_of_sq_sum' {r s : Int} (h : IsCoprime r s) : IsCoprime (HAdd.hAdd (HPow.hPow r 2) (HPow.hPow s 2)) (HMul.hMul r s)

Alias of Int.isCoprime_of_sq_sum'.

theorem Fermat42.not_minimal {a b c : Int} (h : Minimal a b c) (ha2 : Eq (HMod.hMod a 2) 1) (hc : LT.lt 0 c) : False

theorem not_fermat_42 {a b c : Int} (ha : Ne a 0) (hb : Ne b 0) : Ne (HAdd.hAdd (HPow.hPow a 4) (HPow.hPow b 4)) (HPow.hPow c 2)

theorem fermatLastTheoremFour : FermatLastTheoremFor 4

Fermat's Last Theorem for $n=4$: if a b c : ℕ are all non-zero then a ^ 4 + b ^ 4 ≠ c ^ 4.

theorem FermatLastTheorem.of_odd_primes (hprimes : ∀ (p : Nat), Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem

To prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.