mathlib3 documentation

number_theory.fermat4

Fermat's Last Theorem for the case n = 4 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. There are no non-zero integers a, b and c such that a ^ 4 + b ^ 4 = c ^ 4.

def fermat_42 (a b c : ℤ) :

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

fermat_42 a b c = (a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2)

theorem fermat_42.comm {a b c : ℤ} :

fermat_42 a b c ↔ fermat_42 b a c

theorem fermat_42.mul {a b c k : ℤ} (hk0 : k ≠ 0) :

fermat_42 a b c ↔ fermat_42 (k * a) (k * b) (k ^ 2 * c)

theorem fermat_42.ne_zero {a b c : ℤ} (h : fermat_42 a b c) :

c ≠ 0

def fermat_42.minimal (a b c : ℤ) :

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

fermat_42.minimal a b c = (fermat_42 a b c ∧ ∀ (a1 b1 c1 : ℤ), fermat_42 a1 b1 c1 → c.nat_abs ≤ c1.nat_abs)

theorem fermat_42.exists_minimal {a b c : ℤ} (h : fermat_42 a b c) :

∃ (a0 b0 c0 : ℤ), fermat_42.minimal a0 b0 c0

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

theorem fermat_42.coprime_of_minimal {a b c : ℤ} (h : fermat_42.minimal a b c) :

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

theorem fermat_42.minimal_comm {a b c : ℤ} :

fermat_42.minimal a b c → fermat_42.minimal b a c

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

theorem fermat_42.neg_of_minimal {a b c : ℤ} :

fermat_42.minimal a b c → fermat_42.minimal a b (-c)

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

theorem fermat_42.exists_odd_minimal {a b c : ℤ} (h : fermat_42 a b c) :

∃ (a0 b0 c0 : ℤ), fermat_42.minimal a0 b0 c0 ∧ a0 % 2 = 1

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

theorem fermat_42.exists_pos_odd_minimal {a b c : ℤ} (h : fermat_42 a b c) :

∃ (a0 b0 c0 : ℤ), fermat_42.minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

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

theorem int.coprime_of_sq_sum {r s : ℤ} (h2 : is_coprime s r) :

is_coprime (r ^ 2 + s ^ 2) r

theorem int.coprime_of_sq_sum' {r s : ℤ} (h : is_coprime r s) :

is_coprime (r ^ 2 + s ^ 2) (r * s)

theorem fermat_42.not_minimal {a b c : ℤ} (h : fermat_42.minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) :

theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :

a ^ 4 + b ^ 4 ≠ c ^ 2

theorem not_fermat_4 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :

a ^ 4 + b ^ 4 ≠ c ^ 4