internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.ex_fin_div
Proof state before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑(ζ ^ ((2 * k - 1) % ↑p).natAbs) = ↑(↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹)
Tactic:
simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow,
  IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
Proof state after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs =
    ζ' ^ (2 * k) * ζ'⁻¹
Theorem: FltRegular.ex_fin_div
Proof state before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs =
    ζ' ^ (2 * k) * ζ'⁻¹
Tactic:
refine eq_of_div_eq_one ?_
Proof state after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs /
      (ζ' ^ (2 * k) * ζ'⁻¹) =
    1
Theorem: FltRegular.ex_fin_div
Proof state before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs /
      (ζ' ^ (2 * k) * ζ'⁻¹) =
    1
Tactic:
rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
  zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
Proof state after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑((2 * k - 1) % ↑p).natAbs - (2 * k - 1)
Theorem: FltRegular.ex_fin_div
Proof state before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑((2 * k - 1) % ↑p).natAbs - (2 * k - 1)
Tactic:
simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
  Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, Int.cast_one, sub_self]
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have h0 : 0 < p := by linarith
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have h1 : 1 < p := by linarith
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
let s := ({0, 1, k₁.1, k₂.1} : Finset ℕ)
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have : s.card ≤ 4 := by
  repeat refine' le_trans (card_insert_le _ _) (succ_le_succ _)
  exact rfl.ge
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card ≤ 4
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card ≤ 4
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
replace this : s.card < 5 := lt_of_le_of_lt this (by norm_num)
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hs : s ⊆ range p := insert_subset_iff.2 ⟨mem_range.2 h0, insert_subset_iff.2
  ⟨mem_range.2 h1, insert_subset_iff.2 ⟨mem_range.2 (Fin.is_lt _),
  singleton_subset_iff.2 (mem_range.2 (Fin.is_lt _))⟩⟩⟩
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hcard := card_sdiff hs
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
replace hcard : (range p \ s).Nonempty := by
  rw [← Finset.card_pos, hcard, card_range]
  exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).Nonempty
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).Nonempty
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
obtain ⟨i, hi⟩ := hcard
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
refine' ⟨i, sdiff_subset hi, _⟩
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
⊢ f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
⊢ f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
⊢ f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hik₂ : i ≠ k₂ := fun h => by simp [h, s] at hi
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
hik₂ : i ≠ ↑k₂
⊢ f a b (↑k₁) (↑k₂) i = 0
Theorem: FltRegular.auxf'
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
hik₂ : i ≠ ↑k₂
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
simp [f, hi0, hi1, hik₁, hik₂]
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ 0 < p
Tactic:
linarith
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ 1 < p
Tactic:
linarith
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ s.card ≤ 4
Tactic:
repeat refine' le_trans (card_insert_le _ _) (succ_le_succ _)
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₂}.card ≤ 1
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₂}.card ≤ 1
Tactic:
exact rfl.ge
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₁, ↑k₂}.card ≤ 2
Tactic:
refine' le_trans (card_insert_le _ _) (succ_le_succ _)
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₂}.card ≤ 1
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card ≤ 4
⊢ 4 < 5
Tactic:
norm_num
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ (range p \ s).Nonempty
Tactic:
rw [← Finset.card_pos, hcard, card_range]
Proof state after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ 0 < p - s.card
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ 0 < p - s.card
Tactic:
exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
h : i = 0
⊢ False
Tactic:
simp [h, s] at hi
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
h : i = 1
⊢ False
Tactic:
simp [h, s] at hi
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
h : i = ↑k₁
⊢ False
Tactic:
simp [h, s] at hi
Proof state after:
no goals
Theorem: FltRegular.auxf'
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
h : i = ↑k₂
⊢ False
Tactic:
simp [h, s] at hi
Proof state after:
no goals
Theorem: FltRegular.auxf
Proof state before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ ∃ i, f a b ↑k₁ ↑k₂ ↑i = 0
Tactic:
obtain ⟨i, hrange, hi⟩ := auxf' hp5 a b k₁ k₂
Proof state after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
i : ℕ
hrange : i ∈ range p
hi : f a b (↑k₁) (↑k₂) i = 0
⊢ ∃ i, f a b ↑k₁ ↑k₂ ↑i = 0
Theorem: FltRegular.auxf
Proof state before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
i : ℕ
hrange : i ∈ range p
hi : f a b (↑k₁) (↑k₂) i = 0
⊢ ∃ i, f a b ↑k₁ ↑k₂ ↑i = 0
Tactic:
exact ⟨⟨i, mem_range.1 hrange⟩, hi⟩
Proof state after:
no goals
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
⊢ a ^ p + b ^ p ≠ c ^ p
Tactic:
have hcycl : IsCyclotomicExtension {P} ℤ (𝓞 (CyclotomicField P ℚ)) := by
  apply @IsCyclotomicExtension.ring_of_integers' _ _ _ _ (by exact hpri) _
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ a ^ p + b ^ p ≠ c ^ p
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ a ^ p + b ^ p ≠ c ^ p
Tactic:
set ζ := zeta P ℤ R
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ a ^ p + b ^ p ≠ c ^ p
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ a ^ p + b ^ p ≠ c ^ p
Tactic:
have hζ := zeta_spec P ℤ R
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
⊢ a ^ p + b ^ p ≠ c ^ p
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
⊢ a ^ p + b ^ p ≠ c ^ p
Tactic:
intro H
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
⊢ False
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
⊢ False
Tactic:
obtain ⟨k₁, k₂, hcong, hdiv⟩ := ex_fin_div hp5 hreg hζ hgcd caseI H
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
⊢ False
Theorem: FltRegular.caseI_easier
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
⊢ False
Tactic:
have key : ↑(p : ℤ) ∣ ∑ j in range p, f a b k₁ k₂ j • ζ ^ j := by
  convert hdiv using 1
  have h01 : 0 ≠ 1 := zero_ne_one
  have h0k₁ := aux0k₁ hpri.out hp5 hζ caseI hcong hdiv
  have h0k₂ := aux0k₂ hpri.out hp5 hζ hab hcong hdiv
  have h1k₁ := aux1k₁ hpri.out hp5 hζ hab hcong hdiv
  have h1k₂ := aux1k₂ hpri.out hp5 hζ caseI hcong hdiv
  have hk₁k₂ : (k₁ : ℕ) ≠ (k₂ : ℕ) := auxk₁k₂ hpri.out hcong
  simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h01, and_assoc,
    ne_and_eq_iff_right h1k₁, ne_and_eq_iff_right h0k₁, ne_and_eq_iff_right hk₁k₂,
    ne_and_eq_iff_right h1k₂, ne_and_eq_iff_right h0k₂, Finset.range_filter_eq]
  simp only [hpri.out.pos, hpri.out.one_lt, if_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero,
    mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne, zero_smul, sum_const_zero,
    add_zero]
  ring
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j
⊢ False