def FltSolution (n : ℕ) (a : ℤ) (b : ℤ) (c : ℤ) : Prop

solutions to Fermat's last theorem for the exponent 3.

Equations

• FltSolution n a b c = (a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ a ^ n + b ^ n = c ^ n)

def FltCoprime (n : ℕ) (a : ℤ) (b : ℤ) (c : ℤ) : Prop

Coprime solutions to Fermat's last theorem for the exponent 3.

Equations

• FltCoprime n a b c = (FltSolution n a b c ∧ IsCoprime a b ∧ IsCoprime a c ∧ IsCoprime b c)

theorem exists_coprime {n : ℕ} (hn : 0 < n) {a : ℤ} {b : ℤ} {c : ℤ} (ha' : a ≠ 0) (hb' : b ≠ 0) (hc' : c ≠ 0) (h : a ^ n + b ^ n = c ^ n) : ∃ a' b' c', Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

theorem descent1a {a : ℤ} {b : ℤ} {c : ℤ} (h : a ^ 3 + b ^ 3 = c ^ 3) (habcoprime : IsCoprime a b) (haccoprime : IsCoprime a c) (hbccoprime : IsCoprime b c) : (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c

theorem flt_not_add_self {a : ℤ} {b : ℤ} {c : ℤ} (ha : a ≠ 0) (h : a ^ 3 + b ^ 3 = c ^ 3) : a ≠ b

theorem descent1left {a : ℤ} {b : ℤ} {c : ℤ} (hapos : a ≠ 0) (h : a ^ 3 + b ^ 3 = c ^ 3) (hbccoprime : IsCoprime b c) (hb : ¬Even b) (hc : ¬Even c) : ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3

theorem descent1 (a : ℤ) (b : ℤ) (c : ℤ) (h : FltCoprime 3 a b c) : ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3)

theorem descent11 {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (h : d = a ∨ d = b ∨ d = c) : d ∣ a * b * c

theorem descent2 (a : ℤ) (b : ℤ) (c : ℤ) (h : FltCoprime 3 a b c) : ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧ Int.natAbs (2 * p) < Int.natAbs (a ^ 3 * b ^ 3 * c ^ 3)

theorem Nat.cast_three {R : Type u_1} [AddMonoidWithOne R] : ↑3 = 3

theorem gcd1or3 (p : ℤ) (q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : Even p ↔ ¬Even q) : Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 1 ∨ Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 3

theorem obscure' (p : ℤ) (q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : Even p ↔ ¬Even q) (hcube : ∃ r, p ^ 2 + 3 * q ^ 2 = r ^ 3) : ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)

theorem Int.eq_pow_of_mul_eq_pow_odd {a : ℤ} {b : ℤ} {c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) : (∃ d, a = d ^ k) ∧ ∃ e, b = e ^ k

theorem Int.cube_of_coprime (a : ℤ) (b : ℤ) (c : ℤ) (s : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hcoprimeab : IsCoprime a b) (hcoprimeac : IsCoprime a c) (hcoprimebc : IsCoprime b c) (hs : a * b * c = s ^ 3) : ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3

theorem Int.gcd1_coprime12 (u : ℤ) (v : ℤ) (huvcoprime : IsCoprime u v) (notdvd_2_2 : ¬2 ∣ u - 3 * v) (not_3_dvd_2 : ¬3 ∣ u - 3 * v) : IsCoprime (2 * u) (u - 3 * v)

theorem Int.gcd1_coprime13 (u : ℤ) (v : ℤ) (huvcoprime : IsCoprime u v) (this' : ¬Even (u + 3 * v)) (notdvd_3_3 : ¬3 ∣ u + 3 * v) : IsCoprime (2 * u) (u + 3 * v)

theorem Int.gcd1_coprime23 (u : ℤ) (v : ℤ) (huvcoprime : IsCoprime u v) (notdvd_2_2 : ¬2 ∣ u - 3 * v) (notdvd_3_3 : ¬3 ∣ u + 3 * v) : IsCoprime (u - 3 * v) (u + 3 * v)

theorem descent_gcd1 (a : ℤ) (b : ℤ) (c : ℤ) (p : ℤ) (q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hodd : Even p ↔ ¬Even q) (hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) (hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)) : ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

theorem gcd3_coprime {u : ℤ} {v : ℤ} (huvcoprime : IsCoprime u v) (huvodd : Even u ↔ ¬Even v) : IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v)

theorem descent_gcd3_coprime {q : ℤ} {s : ℤ} (h3_ndvd_q : ¬3 ∣ q) (hspos : s ≠ 0) (hcoprime' : IsCoprime s q) (hodd' : Even q ↔ ¬Even s) : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)

theorem descent_gcd3 (a : ℤ) (b : ℤ) (c : ℤ) (p : ℤ) (q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime : IsCoprime p q) (hodd : Even p ↔ ¬Even q) (hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) (hgcd : Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 3) : ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' ^ 3 * b' ^ 3 * c' ^ 3) ≤ Int.natAbs (2 * p) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

theorem descent (a : ℤ) (b : ℤ) (c : ℤ) (h : FltCoprime 3 a b c) : ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ Int.natAbs (a' * b' * c') < Int.natAbs (a * b * c) ∧ a' ^ 3 + b' ^ 3 = c' ^ 3

theorem flt_three : FermatLastTheoremWith ℤ 3