Fermat Last Theorem in the case n = 3

The goal of this file is to prove Fermat Last theorem in the case n = 3.

Main results

• fermatLastTheoremThree_case1: the first case of Fermat Last Theorem when n = 3: if a b c : ℤ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.

TODO

Prove case 2.

theorem fermatLastTheoremThree_case_1 {a : ℤ} {b : ℤ} {c : ℤ} (hdvd : ¬3 ∣ a * b * c) : a ^ 3 + b ^ 3 ≠ c ^ 3

If a b c : ℤ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.

theorem fermatLastTheoremThree_of_three_dvd_only_c (H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) : FermatLastTheoremFor 3

To prove Fermat's Last Theorem for n = 3, it is enough to show that that for all a, b, c in ℤ such that c ≠ 0, ¬ 3 ∣ a, ¬ 3 ∣ b, a and b are coprime and 3 ∣ c, we have a ^ 3 + b ^ 3 ≠ c ^ 3.