def FltRegular.CaseII.Statement : Prop

Statement of case II.

Equations

• FltRegular.CaseII.Statement = ∀ ⦃a b c : ℤ⦄ ⦃p : ℕ⦄ [hp : Fact (Nat.Prime p)], IsRegularPrime p → p ≠ 2 → a * b * c ≠ 0 → ↑p ∣ a * b * c → a ^ p + b ^ p ≠ c ^ p

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

theorem FltRegular.not_exists_solution' {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) : ¬∃ x y z, ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y ∧ ↑(IsPrimitiveRoot.unit' hζ) - 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, Finset.gcd {x, y, z} id = 1 ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p

theorem FltRegular.Int.gcd_left_comm (a : ℤ) (b : ℤ) (c : ℤ) : Int.gcd a ↑(Int.gcd b c) = Int.gcd b ↑(Int.gcd a c)

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

CaseII.