theorem FltRegular.CaseI.two_lt {p : ℕ} (hp5 : 5 ≤ p) : 2 < p

theorem FltRegular.CaseI.aux_cong0k₁ {p : ℕ} (hpri : Nat.Prime p) {k : Fin p} (hcong : ↑↑k ≡ -1 [ZMOD ↑p]) : k = { val := Nat.pred p, isLt := (_ : Nat.pred p < p) }

def FltRegular.CaseI.f0k₁ (b : ℤ) (p : ℕ) : ℕ → ℤ

Auxiliary function.

Equations

• FltRegular.CaseI.f0k₁ b p x = if x = 1 then b else if x = Nat.pred p then -b else 0

theorem FltRegular.CaseI.auxf0k₁ {p : ℕ} (hpri : Nat.Prime p) (hp5 : 5 ≤ p) (b : ℤ) : ∃ i, FltRegular.CaseI.f0k₁ b p ↑i = 0

theorem FltRegular.CaseI.aux0k₁ {p : ℕ} (hpri : Nat.Prime p) {a : ℤ} {b : ℤ} {c : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (caseI : ¬↑p ∣ a * b * c) {k₁ : Fin p} {k₂ : Fin p} (hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]) (hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂) : 0 ≠ ↑k₁

def FltRegular.CaseI.f0k₂ (a : ℤ) (b : ℤ) : ℕ → ℤ

Auxiliary function

Equations

• FltRegular.CaseI.f0k₂ a b x = if x = 0 then a - b else if x = 1 then b - a else 0

theorem FltRegular.CaseI.aux_cong0k₂ {p : ℕ} (hpri : Nat.Prime p) {k : Fin p} (hcong : ↑↑k ≡ 1 [ZMOD ↑p]) : k = { val := 1, isLt := (_ : 1 < p) }

theorem FltRegular.CaseI.auxf0k₂ {p : ℕ} (hpri : Nat.Prime p) (hp5 : 5 ≤ p) (a : ℤ) (b : ℤ) : ∃ i, FltRegular.CaseI.f0k₂ a b ↑i = 0

theorem FltRegular.CaseI.aux0k₂ {p : ℕ} (hpri : Nat.Prime p) {a : ℤ} {b : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (hab : ¬a ≡ b [ZMOD ↑p]) {k₁ : Fin p} {k₂ : Fin p} (hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]) (hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂) : 0 ≠ ↑k₂

theorem FltRegular.CaseI.aux_cong1k₁ {p : ℕ} (hpri : Nat.Prime p) {k : Fin p} (hcong : ↑↑k ≡ 0 [ZMOD ↑p]) : k = { val := 0, isLt := (_ : 0 < p) }

theorem FltRegular.CaseI.aux1k₁ {p : ℕ} (hpri : Nat.Prime p) {a : ℤ} {b : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (hab : ¬a ≡ b [ZMOD ↑p]) {k₁ : Fin p} {k₂ : Fin p} (hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]) (hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂) : 1 ≠ ↑k₁

def FltRegular.CaseI.f1k₂ (a : ℤ) : ℕ → ℤ

Auxiliary function

Equations

• FltRegular.CaseI.f1k₂ a x = if x = 0 then a else if x = 2 then -a else 0

theorem FltRegular.CaseI.aux_cong1k₂ {p : ℕ} {k : Fin p} (hpri : Nat.Prime p) (hp5 : 5 ≤ p) (hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]) : k = { val := 2, isLt := (_ : 2 < p) }

theorem FltRegular.CaseI.auxf1k₂ {p : ℕ} (hpri : Nat.Prime p) (a : ℤ) : ∃ i, FltRegular.CaseI.f1k₂ a ↑i = 0

theorem FltRegular.CaseI.aux1k₂ {p : ℕ} (hpri : Nat.Prime p) {a : ℤ} {b : ℤ} {c : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (caseI : ¬↑p ∣ a * b * c) {k₁ : Fin p} {k₂ : Fin p} (hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]) (hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂) : 1 ≠ ↑k₂

theorem FltRegular.CaseI.auxk₁k₂ {p : ℕ} {k₁ : Fin p} {k₂ : Fin p} (hpri : Nat.Prime p) (hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]) : ↑k₁ ≠ ↑k₂