Theorem: FltRegular.CaseI.aux1k₂ (FltRegular/CaseI/AuxLemmas.lean)

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ 1 ≠ ↑k₂
Tactic:
haveI := (⟨hpri⟩ : Fact (P : ℕ).Prime)
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ 1 ≠ ↑k₂

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ 1 ≠ ↑k₂
Tactic:
symm
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ↑k₂ ≠ 1

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ↑k₂ ≠ 1
Tactic:
intro habs
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
⊢ False
Tactic:
replace hcong := hcong.symm
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ False
Tactic:
rw [show (k₂ : ℤ) = 1 by simpa using habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub,
  sub_eq_iff_eq_add, ← Int.cast_add, ZMod.intCast_eq_intCast_iff] at hcong
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False
Tactic:
rw [habs, pow_one, aux_cong1k₂ hpri hp5 hcong] at hdiv
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨2, ⋯⟩ - ↑b * ζ
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨2, ⋯⟩ - ↑b * ζ
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False
Tactic:
ring_nf at hdiv
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ False
Tactic:
have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by
  suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
    rwa [this]
  simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
    (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]
  simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul,
sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
  ring
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
⊢ False
Tactic:
rw [sum_range] at key
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ False

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ False
Tactic:
refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ ↑p ∣ a

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ ↑p ∣ a
Tactic:
have hpri₁ : (P : ℕ).Prime := hpri
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a
Tactic:
simpa [f1k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf1k₂ hpri a) key ⟨0, hpri.pos⟩
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ ↑↑k₂ = 1
Tactic:
simpa using habs
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
Tactic:
suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
  rwa [this]
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2
Tactic:
simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
  (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 2 < p then {2} else ∅, -a • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 2) (range p), 0 • ζ ^ x) =
    ↑a - ↑a * ζ ^ 2

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 2 < p then {2} else ∅, -a • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 2) (range p), 0 • ζ ^ x) =
    ↑a - ↑a * ζ ^ 2
Tactic:
simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul,
sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
State after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ↑a + -(↑a * ζ ^ 2) = ↑a - ↑a * ζ ^ 2

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ↑a + -(↑a * ζ ^ 2) = ↑a - ↑a * ζ ^ 2
Tactic:
ring
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this✝ : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
this : ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2
⊢ ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
Tactic:
rwa [this]
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ 0 ≠ 2
Tactic:
norm_num
State after:
no goals