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
Fermat42.exists_minimal
{a : ℤ}
{b : ℤ}
{c : ℤ}
(h : Fermat42 a b c)
:
∃ a0 b0 c0, Fermat42.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 : ℤ}
(h : Fermat42.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 : ℤ}
:
Fermat42.Minimal a b c → Fermat42.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 : ℤ}
:
Fermat42.Minimal a b c → Fermat42.Minimal a b (-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 : ℤ}
(h : Fermat42 a b c)
:
∃ a0 b0 c0, Fermat42.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
Fermat42.not_minimal
{a : ℤ}
{b : ℤ}
{c : ℤ}
(h : Fermat42.Minimal a b c)
(ha2 : a % 2 = 1)
(hc : 0 < c)
: