Reductions for Fermat's Last Theorem

This file develops primitive and coprimality reductions used in the regular-prime argument.

theorem FltRegular.MayAssume.coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a * b * c ≠ 0) : (a / {a, b, c}.gcd id) ^ n + (b / {a, b, c}.gcd id) ^ n = (c / {a, b, c}.gcd id) ^ n ∧ {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1 ∧ a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0

theorem FltRegular.p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : Nat.Prime p) (hp : p ≠ 3) (h : a ^ p + b ^ p = c ^ p) (hab : a ≡ b [ZMOD ↑p]) (hbc : b ≡ -c [ZMOD ↑p]) : ↑p ∣ c

theorem FltRegular.a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : Nat.Prime p) (hp5 : 5 ≤ p) (hprod : a * b * c ≠ 0) (h : a ^ p + b ^ p = c ^ p) (hgcd : {a, b, c}.gcd id = 1) (caseI : ¬↑p ∣ a * b * c) : ∃ (x : ℤ) (y : ℤ) (z : ℤ), x ^ p + y ^ p = z ^ p ∧ {x, y, z}.gcd id = 1 ∧ ¬x ≡ y [ZMOD ↑p] ∧ x * y * z ≠ 0 ∧ ¬↑p ∣ x * y * z