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
.
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.
a minimal solution to a ^ 4 + b ^ 4 = c ^ 2
must have a
and b
coprime.
We can swap a
and b
in a minimal solution to a ^ 4 + b ^ 4 = c ^ 2
.
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.not_minimal
{a b c : ℤ}
(h : fermat_42.minimal a b c)
(ha2 : a % 2 = 1)
(hc : 0 < c) :