The second case of Fermat's Last Theorem for regular primes

This file states the second-case contradiction in the cyclotomic-number-field setting.

theorem FltRegular.not_exists_solution {K : Type} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup (NumberField.RingOfIntegers K))] (hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K)))) {ζ : K} (hζ : IsPrimitiveRoot ζ p) {m : ℕ} (hm : 1 ≤ m) : ¬∃ (x' : NumberField.RingOfIntegers K) (y' : NumberField.RingOfIntegers K) (z' : NumberField.RingOfIntegers K) (ε₃ : (NumberField.RingOfIntegers K)ˣ), ¬hζ.toInteger - 1 ∣ y' ∧ ¬hζ.toInteger - 1 ∣ z' ∧ x' ^ p + y' ^ p = ↑ε₃ * ((hζ.toInteger - 1) ^ m * z') ^ p

theorem FltRegular.not_exists_solution' {K : Type} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup (NumberField.RingOfIntegers K))] (hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K)))) {ζ : K} (hζ : IsPrimitiveRoot ζ p) : ¬∃ (x : NumberField.RingOfIntegers K) (y : NumberField.RingOfIntegers K) (z : NumberField.RingOfIntegers K), ¬hζ.toInteger - 1 ∣ y ∧ hζ.toInteger - 1 ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p

theorem FltRegular.not_exists_Int_solution {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (hodd : p ≠ 2) : ¬∃ (x : ℤ) (y : ℤ) (z : ℤ), ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p

theorem FltRegular.not_exists_Int_solution' {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (hodd : p ≠ 2) : ¬∃ (x : ℤ) (y : ℤ) (z : ℤ), {x, y, z}.gcd id = 1 ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p

theorem FltRegular.caseII {a b c : ℤ} {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (hodd : p ≠ 2) (hprod : a * b * c ≠ 0) (hgcd : {a, b, c}.gcd id = 1) (caseII : ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p

Case II of Fermat's Last Theorem for regular primes.