[GOAL]
R : Type u_1
inst✝ : CommRing R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ eval 1 (cyclotomic p R) = ↑p
[PROOFSTEP]
simp only [cyclotomic_prime, eval_X, one_pow, Finset.sum_const, eval_pow, eval_finset_sum, Finset.card_range,
  smul_one_eq_coe]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Semiring S
f : R →+* S
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic p R) = ↑p
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ eval 1 (cyclotomic (p ^ (k + 1)) R) = ↑p
[PROOFSTEP]
simp only [cyclotomic_prime_pow_eq_geom_sum hn.out, eval_X, one_pow, Finset.sum_const, eval_pow, eval_finset_sum,
  Finset.card_range, smul_one_eq_coe]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Semiring S
f : R →+* S
p k : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = ↑p
[PROOFSTEP]
simp
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
⊢ 0 < eval (-1) (cyclotomic n R)
[PROOFSTEP]
haveI := NeZero.of_gt hn
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
⊢ 0 < eval (-1) (cyclotomic n R)
[PROOFSTEP]
rw [← map_cyclotomic_int, ← Int.cast_one, ← Int.cast_neg, eval_int_cast_map, Int.coe_castRingHom, Int.cast_pos]
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)
[PROOFSTEP]
suffices 0 < eval (↑(-1 : ℤ)) (cyclotomic n ℝ)
  by
  rw [← map_cyclotomic_int n ℝ, eval_int_cast_map, Int.coe_castRingHom] at this
  simpa only [Int.cast_pos] using this
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
this : 0 < eval (↑(-1)) (cyclotomic n ℝ)
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)
[PROOFSTEP]
rw [← map_cyclotomic_int n ℝ, eval_int_cast_map, Int.coe_castRingHom] at this
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
this : 0 < (fun x => ↑x) (eval (↑(-1)) (cyclotomic n ℤ))
⊢ 0 < eval (↑(-1)) (cyclotomic n ℤ)
[PROOFSTEP]
simpa only [Int.cast_pos] using this
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
⊢ 0 < eval (↑(-1)) (cyclotomic n ℝ)
[PROOFSTEP]
simp only [Int.cast_one, Int.cast_neg]
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
⊢ 0 < eval (-1) (cyclotomic n ℝ)
[PROOFSTEP]
have h0 := cyclotomic_coeff_zero ℝ hn.le
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
h0 : coeff (cyclotomic n ℝ) 0 = 1
⊢ 0 < eval (-1) (cyclotomic n ℝ)
[PROOFSTEP]
rw [coeff_zero_eq_eval_zero] at h0
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
⊢ 0 < eval (-1) (cyclotomic n ℝ)
[PROOFSTEP]
by_contra' hx
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
⊢ False
[PROOFSTEP]
have := intermediate_value_univ (-1) 0 (cyclotomic n ℝ).continuous
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)
⊢ False
[PROOFSTEP]
obtain ⟨y, hy : IsRoot _ y⟩ := this (show (0 : ℝ) ∈ Set.Icc _ _ by simpa [h0] using hx)
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)
⊢ 0 ∈ Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ))
[PROOFSTEP]
simpa [h0] using hx
[GOAL]
case intro
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)
y : ℝ
hy : IsRoot (cyclotomic n ℝ) y
⊢ False
[PROOFSTEP]
rw [@isRoot_cyclotomic_iff] at hy
[GOAL]
case intro
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)
y : ℝ
hy : IsPrimitiveRoot y n
⊢ False
[PROOFSTEP]
rw [hy.eq_orderOf] at hn
[GOAL]
case intro
n : ℕ
R : Type u_1
inst✝ : LinearOrderedCommRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)
y : ℝ
hn : 2 < orderOf y
hy : IsPrimitiveRoot y n
⊢ False
[PROOFSTEP]
exact hn.not_le LinearOrderedRing.orderOf_le_two
[GOAL]
n : ℕ
hn : 2 < n
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n ih
[GOAL]
case h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
have hn' : 0 < n := pos_of_gt hn
[GOAL]
case h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
have hn'' : 1 < n := one_lt_two.trans hn
[GOAL]
case h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
have := prod_cyclotomic_eq_geom_sum hn' R
[GOAL]
case h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : ∏ i in Finset.erase (divisors n) 1, cyclotomic i R = ∑ i in range n, X ^ i
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
apply_fun eval x at this
[GOAL]
case h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (∏ i in Finset.erase (divisors n) 1, cyclotomic i R) = eval x (∑ i in range n, X ^ i)
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons, eval_mul,
  eval_geom_sum] at this
[GOAL]
case h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
rcases lt_trichotomy 0 (∑ i in Finset.range n, x ^ i) with (h | h | h)
[GOAL]
case h.inl
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 < ∑ i in range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
apply pos_of_mul_pos_left
[GOAL]
case h.inl.h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 < ∑ i in range n, x ^ i
⊢ 0 < eval x (cyclotomic n R) * ?h.inl.b
[PROOFSTEP]
rwa [this]
[GOAL]
case h.inl.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 < ∑ i in range n, x ^ i
⊢ 0 ≤ eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R)
[PROOFSTEP]
rw [eval_prod]
[GOAL]
case h.inl.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 < ∑ i in range n, x ^ i
⊢ 0 ≤ ∏ j in Finset.erase (properDivisors n) 1, eval x (cyclotomic j R)
[PROOFSTEP]
refine' Finset.prod_nonneg fun i hi => _
[GOAL]
case h.inl.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 < ∑ i in range n, x ^ i
i : ℕ
hi : i ∈ Finset.erase (properDivisors n) 1
⊢ 0 ≤ eval x (cyclotomic i R)
[PROOFSTEP]
simp only [Finset.mem_erase, mem_properDivisors] at hi
[GOAL]
case h.inl.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 < ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 ≤ eval x (cyclotomic i R)
[PROOFSTEP]
rw [geom_sum_pos_iff hn'.ne'] at h
[GOAL]
case h.inl.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Odd n ∨ 0 < x + 1
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 ≤ eval x (cyclotomic i R)
[PROOFSTEP]
cases' h with hk hx
[GOAL]
case h.inl.hb.inl
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ 0 ≤ eval x (cyclotomic i R)
[PROOFSTEP]
refine' (ih _ hi.2.2 (Nat.two_lt_of_ne _ hi.1 _)).le
[GOAL]
case h.inl.hb.inl.refine'_1
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ i ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case h.inl.hb.inl.refine'_2
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ i ≠ 2
[PROOFSTEP]
rintro rfl
[GOAL]
case h.inl.hb.inl.refine'_1
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
hk : Odd n
hi : 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False
[PROOFSTEP]
exact hn'.ne' (zero_dvd_iff.mp hi.2.1)
[GOAL]
case h.inl.hb.inl.refine'_2
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
hk : Odd n
hi : 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
⊢ False
[PROOFSTEP]
exact even_iff_not_odd.mp (even_iff_two_dvd.mpr hi.2.1) hk
[GOAL]
case h.inl.hb.inr
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
⊢ 0 ≤ eval x (cyclotomic i R)
[PROOFSTEP]
rcases eq_or_ne i 2 with (rfl | hk)
[GOAL]
case h.inl.hb.inr.inl
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
hx : 0 < x + 1
hi : 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
⊢ 0 ≤ eval x (cyclotomic 2 R)
[PROOFSTEP]
simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le
[GOAL]
case h.inl.hb.inr.inr
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ 0 ≤ eval x (cyclotomic i R)
[PROOFSTEP]
refine' (ih _ hi.2.2 (Nat.two_lt_of_ne _ hi.1 hk)).le
[GOAL]
case h.inl.hb.inr.inr
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ i ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case h.inl.hb.inr.inr
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
hx : 0 < x + 1
hi : 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
hk : 0 ≠ 2
⊢ False
[PROOFSTEP]
exact hn'.ne' <| zero_dvd_iff.mp hi.2.1
[GOAL]
case h.inr.inl
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : 0 = ∑ i in range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h
[GOAL]
case h.inr.inl
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : x = -1 ∧ Even n
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
exact h.1.symm ▸ cyclotomic_neg_one_pos hn
[GOAL]
case h.inr.inr
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : ∑ i in range n, x ^ i < 0
⊢ 0 < eval x (cyclotomic n R)
[PROOFSTEP]
apply pos_of_mul_neg_left
[GOAL]
case h.inr.inr.h
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : ∑ i in range n, x ^ i < 0
⊢ eval x (cyclotomic n R) * ?h.inr.inr.b < 0
[PROOFSTEP]
rwa [this]
[GOAL]
case h.inr.inr.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : ∑ i in range n, x ^ i < 0
⊢ eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) ≤ 0
[PROOFSTEP]
rw [geom_sum_neg_iff hn'.ne'] at h
[GOAL]
case h.inr.inr.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) ≤ 0
[PROOFSTEP]
have h2 : 2 ∈ n.properDivisors.erase 1 :=
  by
  rw [Finset.mem_erase, mem_properDivisors]
  exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
[GOAL]
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ∈ Finset.erase (properDivisors n) 1
[PROOFSTEP]
rw [Finset.mem_erase, mem_properDivisors]
[GOAL]
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
[PROOFSTEP]
exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
[GOAL]
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case h.inr.inr.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
⊢ eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) ≤ 0
[PROOFSTEP]
rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]
[GOAL]
case h.inr.inr.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
⊢ (∏ x_1 in Finset.erase (Finset.erase (properDivisors n) 1) 2, eval x (cyclotomic x_1 R)) * eval x (cyclotomic 2 R) ≤ 0
[PROOFSTEP]
apply mul_nonpos_of_nonneg_of_nonpos
[GOAL]
case h.inr.inr.hb.ha
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
⊢ 0 ≤ ∏ x_1 in Finset.erase (Finset.erase (properDivisors n) 1) 2, eval x (cyclotomic x_1 R)
[PROOFSTEP]
refine' Finset.prod_nonneg fun i hi => le_of_lt _
[GOAL]
case h.inr.inr.hb.ha
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
i : ℕ
hi : i ∈ Finset.erase (Finset.erase (properDivisors n) 1) 2
⊢ 0 < eval x (cyclotomic i R)
[PROOFSTEP]
simp only [Finset.mem_erase, mem_properDivisors] at hi
[GOAL]
case h.inr.inr.hb.ha
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
i : ℕ
hi : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 < eval x (cyclotomic i R)
[PROOFSTEP]
refine' ih _ hi.2.2.2 (Nat.two_lt_of_ne _ hi.2.1 hi.1)
[GOAL]
case h.inr.inr.hb.ha
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
i : ℕ
hi : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ i ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case h.inr.inr.hb.ha
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
hi : 0 ≠ 2 ∧ 0 ≠ 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False
[PROOFSTEP]
rw [zero_dvd_iff] at hi
[GOAL]
case h.inr.inr.hb.ha
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
hi : 0 ≠ 2 ∧ 0 ≠ 1 ∧ n = 0 ∧ 0 < n
⊢ False
[PROOFSTEP]
exact hn'.ne' hi.2.2.1
[GOAL]
case h.inr.inr.hb.hb
n✝ : ℕ
hn✝ : 2 < n✝
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
ih : ∀ (m : ℕ), m < n → 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this :
  eval x (cyclotomic n R) * eval x (∏ x in Finset.erase (properDivisors n) 1, cyclotomic x R) = ∑ i in range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ Finset.erase (properDivisors n) 1
⊢ eval x (cyclotomic 2 R) ≤ 0
[PROOFSTEP]
simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le
[GOAL]
n : ℕ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))
[PROOFSTEP]
rcases n with (_ | _ | _ | n)
[GOAL]
case zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic Nat.zero R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic Nat.zero R))
[PROOFSTEP]
simp [cyclotomic_zero, cyclotomic_one, cyclotomic_two, succ_eq_add_one, eval_X, eval_one, eval_add, eval_sub,
  sub_nonneg, sub_pos, zero_lt_one, zero_le_one, imp_true_iff, imp_self, and_self_iff]
[GOAL]
case succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (succ Nat.zero) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (succ Nat.zero) R))
[PROOFSTEP]
simp [cyclotomic_zero, cyclotomic_one, cyclotomic_two, succ_eq_add_one, eval_X, eval_one, eval_add, eval_sub,
  sub_nonneg, sub_pos, zero_lt_one, zero_le_one, imp_true_iff, imp_self, and_self_iff]
[GOAL]
case succ.succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (succ (succ Nat.zero)) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (succ (succ Nat.zero)) R))
[PROOFSTEP]
simp [cyclotomic_zero, cyclotomic_one, cyclotomic_two, succ_eq_add_one, eval_X, eval_one, eval_add, eval_sub,
  sub_nonneg, sub_pos, zero_lt_one, zero_le_one, imp_true_iff, imp_self, and_self_iff]
[GOAL]
case succ.succ.succ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (succ (succ (succ n))) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (succ (succ (succ n))) R))
[PROOFSTEP]
simp [cyclotomic_zero, cyclotomic_one, cyclotomic_two, succ_eq_add_one, eval_X, eval_one, eval_add, eval_sub,
  sub_nonneg, sub_pos, zero_lt_one, zero_le_one, imp_true_iff, imp_self, and_self_iff]
[GOAL]
case succ.succ.zero
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (1 + 1) R))
[PROOFSTEP]
constructor
[GOAL]
case succ.succ.zero.left
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ 1 < x → 0 < eval x (cyclotomic (1 + 1) R)
[PROOFSTEP]
intro
[GOAL]
case succ.succ.zero.right
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
⊢ 1 ≤ x → 0 ≤ eval x (cyclotomic (1 + 1) R)
[PROOFSTEP]
intro
[GOAL]
case succ.succ.zero.left
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
a✝ : 1 < x
⊢ 0 < eval x (cyclotomic (1 + 1) R)
[PROOFSTEP]
norm_num
[GOAL]
case succ.succ.zero.right
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
a✝ : 1 ≤ x
⊢ 0 ≤ eval x (cyclotomic (1 + 1) R)
[PROOFSTEP]
norm_num
[GOAL]
case succ.succ.zero.left
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
a✝ : 1 < x
⊢ 0 < x + 1
[PROOFSTEP]
linarith
[GOAL]
case succ.succ.zero.right
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
a✝ : 1 ≤ x
⊢ 0 ≤ x + 1
[PROOFSTEP]
linarith
[GOAL]
case succ.succ.succ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (n + 2 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 2 + 1) R))
[PROOFSTEP]
have : 2 < n + 3 := by linarith
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
⊢ 2 < n + 3
[PROOFSTEP]
linarith
[GOAL]
case succ.succ.succ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
⊢ (1 < x → 0 < eval x (cyclotomic (n + 2 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 2 + 1) R))
[PROOFSTEP]
constructor <;> intro <;> [skip; apply le_of_lt]
[GOAL]
case succ.succ.succ
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
⊢ (1 < x → 0 < eval x (cyclotomic (n + 2 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 2 + 1) R))
[PROOFSTEP]
constructor
[GOAL]
case succ.succ.succ.left
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
⊢ 1 < x → 0 < eval x (cyclotomic (n + 2 + 1) R)
[PROOFSTEP]
intro
[GOAL]
case succ.succ.succ.right
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
⊢ 1 ≤ x → 0 ≤ eval x (cyclotomic (n + 2 + 1) R)
[PROOFSTEP]
intro
[GOAL]
case succ.succ.succ.left
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
a✝ : 1 < x
⊢ 0 < eval x (cyclotomic (n + 2 + 1) R)
[PROOFSTEP]
skip
[GOAL]
case succ.succ.succ.right
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
a✝ : 1 ≤ x
⊢ 0 ≤ eval x (cyclotomic (n + 2 + 1) R)
[PROOFSTEP]
apply le_of_lt
[GOAL]
case succ.succ.succ.left
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
a✝ : 1 < x
⊢ 0 < eval x (cyclotomic (n + 2 + 1) R)
[PROOFSTEP]
apply cyclotomic_pos this
[GOAL]
case succ.succ.succ.right.a
R : Type u_1
inst✝ : LinearOrderedCommRing R
x : R
n : ℕ
this : 2 < n + 3
a✝ : 1 ≤ x
⊢ 0 < eval x (cyclotomic (n + 2 + 1) R)
[PROOFSTEP]
apply cyclotomic_pos this
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
⊢ eval 1 (cyclotomic n R) = 1
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn')
[GOAL]
case inl
R : Type u_1
inst✝ : Ring R
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0
⊢ eval 1 (cyclotomic 0 R) = 1
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
⊢ eval 1 (cyclotomic n R) = 1
[PROOFSTEP]
have hn : 1 < n := one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn'.ne', (h Nat.prime_two 0).symm⟩
[GOAL]
case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n R) = 1
[PROOFSTEP]
rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
[GOAL]
case inr.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
⊢ eval 1 (cyclotomic n R) = 1
[PROOFSTEP]
have := eval_int_cast_map (Int.castRingHom R) (cyclotomic n ℤ) 1
[GOAL]
case inr.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
this : eval (↑1) (map (Int.castRingHom R) (cyclotomic n ℤ)) = ↑(Int.castRingHom R) (eval (↑1) (cyclotomic n ℤ))
⊢ eval 1 (cyclotomic n R) = 1
[PROOFSTEP]
simpa only [map_cyclotomic, Int.cast_one, h, eq_intCast] using this
[GOAL]
case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1
[PROOFSTEP]
exfalso
[GOAL]
case inr.inr.h
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ False
[PROOFSTEP]
linarith [cyclotomic_nonneg n (le_refl (1 : ℤ))]
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
[PROOFSTEP]
rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd]
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
[PROOFSTEP]
intro p hp hpe
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
⊢ False
[PROOFSTEP]
haveI := Fact.mk hp
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this : Fact (Nat.Prime p)
⊢ False
[PROOFSTEP]
have := prod_cyclotomic_eq_geom_sum hn' ℤ
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this : ∏ i in Finset.erase (divisors n) 1, cyclotomic i ℤ = ∑ i in range n, X ^ i
⊢ False
[PROOFSTEP]
apply_fun eval 1 at this
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this : eval 1 (∏ i in Finset.erase (divisors n) 1, cyclotomic i ℤ) = eval 1 (∑ i in range n, X ^ i)
⊢ False
[PROOFSTEP]
rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ←
  Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _, Finset.prod_image] at this
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
simp_rw [eval_one_cyclotomic_prime_pow, Finset.prod_const, Finset.card_range, mul_comm] at this
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
rw [← Finset.prod_sdiff <| show { n } ⊆ _ from _] at this
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ)) *
        ∏ x in {n}, eval 1 (cyclotomic x ℤ))
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
swap
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))
[PROOFSTEP]
simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne.def, mem_divisors, dvd_refl, true_and_iff, mem_image,
  mem_range, exists_prop, not_exists, not_and]
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)
⊢ (¬n = 1 ∧ ¬n = 0) ∧ ∀ (x : ℕ), x < padicValNat p n → ¬p ^ (x + 1) = n
[PROOFSTEP]
exact ⟨⟨hn.ne', hn'.ne'⟩, fun t _ => h hp _⟩
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ)) *
        ∏ x in {n}, eval 1 (cyclotomic x ℤ))
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
rw [← Int.natAbs_ofNat p, Int.natAbs_dvd_natAbs] at hpe
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : ↑p ∣ eval 1 (cyclotomic n ℤ)
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ)) *
        ∏ x in {n}, eval 1 (cyclotomic x ℤ))
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
obtain ⟨t, ht⟩ := hpe
[GOAL]
case intro
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ)) *
        ∏ x in {n}, eval 1 (cyclotomic x ℤ))
t : ℤ
ht : eval 1 (cyclotomic n ℤ) = ↑p * t
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
rw [Finset.prod_singleton, ht, mul_left_comm, mul_comm, ← mul_assoc, mul_assoc] at this
[GOAL]
case intro
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this✝ : Fact (Nat.Prime p)
t : ℤ
this :
  ↑n =
    ↑p ^ padicValNat p n * ↑p *
      (t *
        ∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = ↑p * t
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩
[GOAL]
case intro
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this✝¹ : Fact (Nat.Prime p)
t : ℤ
this✝ :
  ↑n =
    ↑p ^ padicValNat p n * ↑p *
      (t *
        ∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = ↑p * t
this : ↑p ^ padicValNat p n * ↑p ∣ ↑n
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
simp only [← _root_.pow_succ', ← Int.natAbs_dvd_natAbs, Int.natAbs_ofNat, Int.natAbs_pow] at this
[GOAL]
case intro
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this✝¹ : Fact (Nat.Prime p)
t : ℤ
this✝ :
  ↑n =
    ↑p ^ padicValNat p n * ↑p *
      (t *
        ∏ x in (Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = ↑p * t
this : p ^ (padicValNat p n + 1) ∣ n
⊢ False
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
exact pow_succ_padicValNat_not_dvd hn'.ne' this
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ ∀ (x : ℕ), x ∈ range (padicValNat p n) → ∀ (y : ℕ), y ∈ range (padicValNat p n) → p ^ (x + 1) = p ^ (y + 1) → x = y
[PROOFSTEP]
rintro x - y - hxy
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
x y : ℕ
hxy : p ^ (x + 1) = p ^ (y + 1)
⊢ x = y
[PROOFSTEP]
apply Nat.succ_injective
[GOAL]
case a
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ Int.natAbs (eval 1 (cyclotomic n ℤ))
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x in Finset.erase (divisors n) 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)),
        eval 1 (cyclotomic x ℤ)) *
      ∏ x in image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
x y : ℕ
hxy : p ^ (x + 1) = p ^ (y + 1)
⊢ succ x = succ y
[PROOFSTEP]
exact Nat.pow_right_injective hp.two_le hxy
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
have hn : 0 < n := pos_of_gt hn'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
have hq := zero_lt_one.trans hq'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖ :=
  by
  intro ζ' hζ'
  rw [mem_primitiveRoots hn] at hζ'
  convert norm_sub_norm_le (↑q) ζ'
  · rw [Complex.norm_real, Real.norm_of_nonneg hq.le]
  · rw [hζ'.norm'_eq_one hn.ne']
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
[PROOFSTEP]
intro ζ' hζ'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ q - 1 ≤ ‖↑q - ζ'‖
[PROOFSTEP]
rw [mem_primitiveRoots hn] at hζ'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q - 1 ≤ ‖↑q - ζ'‖
[PROOFSTEP]
convert norm_sub_norm_le (↑q) ζ'
[GOAL]
case h.e'_3.h.e'_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖↑q‖
[PROOFSTEP]
rw [Complex.norm_real, Real.norm_of_nonneg hq.le]
[GOAL]
case h.e'_3.h.e'_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ 1 = ‖ζ'‖
[PROOFSTEP]
rw [hζ'.norm'_eq_one hn.ne']
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
let ζ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
have hζ : IsPrimitiveRoot ζ n := Complex.isPrimitiveRoot_exp n hn.ne'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
have hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖ :=
  by
  refine' ⟨ζ, (mem_primitiveRoots hn).mpr hζ, _⟩
  suffices ¬SameRay ℝ (q : ℂ) ζ by
    convert lt_norm_sub_of_not_sameRay this <;>
      simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
  rw [Complex.sameRay_iff]
  push_neg
  refine' ⟨by exact_mod_cast hq.ne', hζ.ne_zero hn.ne', _⟩
  rw [Complex.arg_ofReal_of_nonneg hq.le, Ne.def, eq_comm, hζ.arg_eq_zero_iff hn.ne']
  clear_value ζ
  rintro rfl
  linarith [hζ.unique IsPrimitiveRoot.one]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
[PROOFSTEP]
refine' ⟨ζ, (mem_primitiveRoots hn).mpr hζ, _⟩
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ q - 1 < ‖↑q - ζ‖
[PROOFSTEP]
suffices ¬SameRay ℝ (q : ℂ) ζ by
  convert lt_norm_sub_of_not_sameRay this <;>
    simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) ζ
⊢ q - 1 < ‖↑q - ζ‖
[PROOFSTEP]
convert lt_norm_sub_of_not_sameRay this
[GOAL]
case h.e'_3.h.e'_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) ζ
⊢ q = ‖↑q‖
[PROOFSTEP]
simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
[GOAL]
case h.e'_3.h.e'_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) ζ
⊢ 1 = ‖ζ‖
[PROOFSTEP]
simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬SameRay ℝ (↑q) ζ
[PROOFSTEP]
rw [Complex.sameRay_iff]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬(↑q = 0 ∨ ζ = 0 ∨ Complex.arg ↑q = Complex.arg ζ)
[PROOFSTEP]
push_neg
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ↑q ≠ 0 ∧
    Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ≠ 0 ∧
      Complex.arg ↑q ≠ Complex.arg (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
[PROOFSTEP]
refine' ⟨by exact_mod_cast hq.ne', hζ.ne_zero hn.ne', _⟩
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ↑q ≠ 0
[PROOFSTEP]
exact_mod_cast hq.ne'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ Complex.arg ↑q ≠ Complex.arg (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
[PROOFSTEP]
rw [Complex.arg_ofReal_of_nonneg hq.le, Ne.def, eq_comm, hζ.arg_eq_zero_iff hn.ne']
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬ζ = 1
[PROOFSTEP]
clear_value ζ
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
⊢ ¬ζ = 1
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
hζ : IsPrimitiveRoot 1 n
⊢ False
[PROOFSTEP]
linarith [hζ.unique IsPrimitiveRoot.one]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
have : ¬eval (↑q) (cyclotomic n ℂ) = 0 :=
  by
  erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ)]
  simpa only [Complex.coe_algebraMap, Complex.ofReal_eq_zero] using (cyclotomic_pos' n hq').ne'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
⊢ ¬eval (↑q) (cyclotomic n ℂ) = 0
[PROOFSTEP]
erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ)]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
⊢ ¬↑(algebraMap ℝ ℂ) (eval q (cyclotomic n ℝ)) = 0
[PROOFSTEP]
simpa only [Complex.coe_algebraMap, Complex.ofReal_eq_zero] using (cyclotomic_pos' n hq').ne'
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
suffices
  Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq']) ^ totient n < Units.mk0 ‖(cyclotomic n ℂ).eval ↑q‖₊ (by simp [this])
  by
  simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe, hq'.le,
    Real.toNNReal_lt_toNNReal_iff_of_nonneg, coe_nnnorm, Complex.norm_eq_abs, NNReal.coe_pow, Real.coe_toNNReal',
    max_eq_left, sub_nonneg] at this
  convert this
  erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ), eq_comm]
  simp only [cyclotomic_nonneg n hq'.le, Complex.coe_algebraMap, Complex.abs_ofReal, abs_eq_self]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Real.toNNReal (q - 1) ≠ 0
[PROOFSTEP]
simp [hq']
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ‖eval (↑q) (cyclotomic n ℂ)‖₊ ≠ 0
[PROOFSTEP]
simp [this]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this :
  Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) ^ φ n <
    Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ (_ : ¬‖eval (↑q) (cyclotomic n ℂ)‖₊ = 0)
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe, hq'.le,
  Real.toNNReal_lt_toNNReal_iff_of_nonneg, coe_nnnorm, Complex.norm_eq_abs, NNReal.coe_pow, Real.coe_toNNReal',
  max_eq_left, sub_nonneg] at this
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ↑Complex.abs (eval (↑q) (cyclotomic n ℂ))
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ↑Complex.abs (eval (↑q) (cyclotomic n ℂ))
⊢ eval q (cyclotomic n ℝ) = ↑Complex.abs (eval (↑q) (cyclotomic n ℂ))
[PROOFSTEP]
erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ), eq_comm]
[GOAL]
case h.e'_4
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ↑Complex.abs (eval (↑q) (cyclotomic n ℂ))
⊢ ↑Complex.abs (↑(algebraMap ℝ ℂ) (eval q (cyclotomic n ℝ))) = eval q (cyclotomic n ℝ)
[PROOFSTEP]
simp only [cyclotomic_nonneg n hq'.le, Complex.coe_algebraMap, Complex.abs_ofReal, abs_eq_self]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) ^ φ n <
    Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ (_ : ¬‖eval (↑q) (cyclotomic n ℂ)‖₊ = 0)
[PROOFSTEP]
simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub, nnnorm_prod, Units.mk0_prod]
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) ^ φ n <
    ∏ b in attach (primitiveRoots n ℂ), Units.mk0 ‖↑q - ↑b‖₊ (_ : ‖↑q - ↑b‖₊ = 0 → False)
[PROOFSTEP]
convert Finset.prod_lt_prod' (M := NNRealˣ) _ _
[GOAL]
case h.e'_3
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) ^ φ n =
    ∏ i in attach (primitiveRoots n ℂ), ?convert_2 i
case convert_2
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ { x // x ∈ primitiveRoots n ℂ } → NNRealˣ
case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ (i : { x // x ∈ primitiveRoots n ℂ }),
    i ∈ attach (primitiveRoots n ℂ) → ?convert_2 i ≤ Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False)
case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i, i ∈ attach (primitiveRoots n ℂ) ∧ ?convert_2 i < Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False)
[PROOFSTEP]
swap
[GOAL]
case convert_2
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ { x // x ∈ primitiveRoots n ℂ } → NNRealˣ
[PROOFSTEP]
exact fun _ => Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq'])
[GOAL]
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x✝ : { x // x ∈ primitiveRoots n ℂ }
⊢ Real.toNNReal (q - 1) ≠ 0
[PROOFSTEP]
simp [hq']
[GOAL]
case h.e'_3
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) ^ φ n =
    ∏ i in attach (primitiveRoots n ℂ), Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0)
[PROOFSTEP]
simp only [Complex.card_primitiveRoots, prod_const, card_attach]
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ (i : { x // x ∈ primitiveRoots n ℂ }),
    i ∈ attach (primitiveRoots n ℂ) →
      Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) ≤
        Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False)
[PROOFSTEP]
simp only [Subtype.coe_mk, Finset.mem_attach, forall_true_left, Subtype.forall, ← Units.val_le_val, ← NNReal.coe_le_coe,
  Complex.abs.nonneg, hq'.le, Units.val_mk0, Real.coe_toNNReal', coe_nnnorm, Complex.norm_eq_abs, max_le_iff,
  tsub_le_iff_right]
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ (a : ℂ), a ∈ primitiveRoots n ℂ → q ≤ ↑Complex.abs (↑q - a) + 1 ∧ True
[PROOFSTEP]
intro x hx
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
⊢ q ≤ ↑Complex.abs (↑q - x) + 1 ∧ True
[PROOFSTEP]
simpa only [and_true_iff, tsub_le_iff_right] using hfor x hx
[GOAL]
case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i,
    i ∈ attach (primitiveRoots n ℂ) ∧
      Units.mk0 (Real.toNNReal (q - 1)) (_ : ¬Real.toNNReal (q - 1) = 0) <
        Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False)
[PROOFSTEP]
simp only [Subtype.coe_mk, Finset.mem_attach, exists_true_left, Subtype.exists, ← NNReal.coe_lt_coe, ← Units.val_lt_val,
  Units.val_mk0 _, coe_nnnorm]
[GOAL]
case convert_6
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ a h, True ∧ ↑(Real.toNNReal (q - 1)) < ‖↑q - a‖
[PROOFSTEP]
simpa [hq'.le, Real.coe_toNNReal', max_eq_left, sub_nonneg] using hex
[GOAL]
q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 0 ≤ eval q (cyclotomic 0 ℝ)
[PROOFSTEP]
simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]
[GOAL]
q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 1 ≤ eval q (cyclotomic 1 ℝ)
[PROOFSTEP]
simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one, le_refl]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
have hn : 0 < n := pos_of_gt hn'
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
have hq := zero_lt_one.trans hq'
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1 :=
  by
  intro ζ' hζ'
  rw [mem_primitiveRoots hn] at hζ'
  convert norm_sub_le (↑q) ζ'
  · rw [Complex.norm_real, Real.norm_of_nonneg (zero_le_one.trans_lt hq').le]
  · rw [hζ'.norm'_eq_one hn.ne']
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
[PROOFSTEP]
intro ζ' hζ'
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ ‖↑q - ζ'‖ ≤ q + 1
[PROOFSTEP]
rw [mem_primitiveRoots hn] at hζ'
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖↑q - ζ'‖ ≤ q + 1
[PROOFSTEP]
convert norm_sub_le (↑q) ζ'
[GOAL]
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖↑q‖
[PROOFSTEP]
rw [Complex.norm_real, Real.norm_of_nonneg (zero_le_one.trans_lt hq').le]
[GOAL]
case h.e'_4.h.e'_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ 1 = ‖ζ'‖
[PROOFSTEP]
rw [hζ'.norm'_eq_one hn.ne']
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
let ζ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
have hζ : IsPrimitiveRoot ζ n := Complex.isPrimitiveRoot_exp n hn.ne'
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
have hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1 :=
  by
  refine' ⟨ζ, (mem_primitiveRoots hn).mpr hζ, _⟩
  suffices ¬SameRay ℝ (q : ℂ) (-ζ) by
    convert norm_add_lt_of_not_sameRay this using 2
    · rw [Complex.norm_eq_abs, Complex.abs_ofReal]
      symm
      exact abs_eq_self.mpr hq.le
    · simp [abs_of_pos hq, hζ.norm'_eq_one hn.ne', -Complex.norm_eq_abs]
  rw [Complex.sameRay_iff]
  push_neg
  refine' ⟨by exact_mod_cast hq.ne', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', _⟩
  rw [Complex.arg_ofReal_of_nonneg hq.le, Ne.def, eq_comm]
  intro h
  rw [Complex.arg_eq_zero_iff, Complex.neg_re, neg_nonneg, Complex.neg_im, neg_eq_zero] at h
  have hζ₀ : ζ ≠ 0 := by
    clear_value ζ
    rintro rfl
    exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
  have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩
  rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this
  rw [this] at hζ
  linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm]
  · contrapose! hζ₀
    ext <;> simp [hζ₀, h.2]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
[PROOFSTEP]
refine' ⟨ζ, (mem_primitiveRoots hn).mpr hζ, _⟩
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ‖↑q - ζ‖ < q + 1
[PROOFSTEP]
suffices ¬SameRay ℝ (q : ℂ) (-ζ) by
  convert norm_add_lt_of_not_sameRay this using 2
  · rw [Complex.norm_eq_abs, Complex.abs_ofReal]
    symm
    exact abs_eq_self.mpr hq.le
  · simp [abs_of_pos hq, hζ.norm'_eq_one hn.ne', -Complex.norm_eq_abs]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ ‖↑q - ζ‖ < q + 1
[PROOFSTEP]
convert norm_add_lt_of_not_sameRay this using 2
[GOAL]
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ q = ‖↑q‖
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_ofReal]
[GOAL]
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ q = |q|
[PROOFSTEP]
symm
[GOAL]
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ |q| = q
[PROOFSTEP]
exact abs_eq_self.mpr hq.le
[GOAL]
case h.e'_4.h.e'_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) (-ζ)
⊢ 1 = ‖-ζ‖
[PROOFSTEP]
simp [abs_of_pos hq, hζ.norm'_eq_one hn.ne', -Complex.norm_eq_abs]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬SameRay ℝ (↑q) (-ζ)
[PROOFSTEP]
rw [Complex.sameRay_iff]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬(↑q = 0 ∨ -ζ = 0 ∨ Complex.arg ↑q = Complex.arg (-ζ))
[PROOFSTEP]
push_neg
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ↑q ≠ 0 ∧
    -Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ≠ 0 ∧
      Complex.arg ↑q ≠ Complex.arg (-Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
[PROOFSTEP]
refine' ⟨by exact_mod_cast hq.ne', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', _⟩
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ↑q ≠ 0
[PROOFSTEP]
exact_mod_cast hq.ne'
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ Complex.arg ↑q ≠ Complex.arg (-Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
[PROOFSTEP]
rw [Complex.arg_ofReal_of_nonneg hq.le, Ne.def, eq_comm]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬Complex.arg (-Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) = 0
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : Complex.arg (-Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) = 0
⊢ False
[PROOFSTEP]
rw [Complex.arg_eq_zero_iff, Complex.neg_re, neg_nonneg, Complex.neg_im, neg_eq_zero] at h
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
⊢ False
[PROOFSTEP]
have hζ₀ : ζ ≠ 0 := by
  clear_value ζ
  rintro rfl
  exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
⊢ ζ ≠ 0
[PROOFSTEP]
clear_value ζ
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
ζ : ℂ
hζ : IsPrimitiveRoot ζ n
⊢ ζ ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ : IsPrimitiveRoot 0 n
⊢ False
[PROOFSTEP]
exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
⊢ False
[PROOFSTEP]
have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩
[GOAL]
case refine_2
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
this : ζ.re < 0 ∧ ζ.im = 0
⊢ False
case refine_1
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
⊢ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≠ 0
[PROOFSTEP]
rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this
[GOAL]
case refine_2
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ False
case refine_1
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
⊢ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≠ 0
[PROOFSTEP]
rw [this] at hζ
[GOAL]
case refine_2
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot (-1) n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ False
case refine_1
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
⊢ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≠ 0
[PROOFSTEP]
linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm]
[GOAL]
case refine_1
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : ζ ≠ 0
⊢ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≠ 0
[PROOFSTEP]
contrapose! hζ₀
[GOAL]
case refine_1
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re = 0
⊢ Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) = 0
[PROOFSTEP]
ext
[GOAL]
case refine_1.a
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re = 0
⊢ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re = 0.re
[PROOFSTEP]
simp [hζ₀, h.2]
[GOAL]
case refine_1.a
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
h : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re ≤ 0 ∧ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0
hζ₀ : (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).re = 0
⊢ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)).im = 0.im
[PROOFSTEP]
simp [hζ₀, h.2]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
have : ¬eval (↑q) (cyclotomic n ℂ) = 0 :=
  by
  erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ)]
  simp only [Complex.coe_algebraMap, Complex.ofReal_eq_zero]
  exact (cyclotomic_pos' n hq').ne.symm
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
⊢ ¬eval (↑q) (cyclotomic n ℂ) = 0
[PROOFSTEP]
erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ)]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
⊢ ¬↑(algebraMap ℝ ℂ) (eval q (cyclotomic n ℝ)) = 0
[PROOFSTEP]
simp only [Complex.coe_algebraMap, Complex.ofReal_eq_zero]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
⊢ ¬eval q (cyclotomic n ℝ) = 0
[PROOFSTEP]
exact (cyclotomic_pos' n hq').ne.symm
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
suffices
  Units.mk0 ‖(cyclotomic n ℂ).eval ↑q‖₊ (by simp [this]) <
    Units.mk0 (Real.toNNReal (q + 1)) (by simp; linarith) ^ totient n
  by
  simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe, hq'.le,
    Real.toNNReal_lt_toNNReal_iff_of_nonneg, coe_nnnorm, Complex.norm_eq_abs, NNReal.coe_pow, Real.coe_toNNReal',
    max_eq_left, sub_nonneg] at this
  convert this using 2
  · erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ), eq_comm]
    simp [cyclotomic_nonneg n hq'.le]
  rw [eq_comm, max_eq_left_iff]
  linarith
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ‖eval (↑q) (cyclotomic n ℂ)‖₊ ≠ 0
[PROOFSTEP]
simp [this]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Real.toNNReal (q + 1) ≠ 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ 0 < q + 1
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this :
  Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ (_ : ¬‖eval (↑q) (cyclotomic n ℂ)‖₊ = 0) <
    Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0) ^ φ n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe, hq'.le,
  Real.toNNReal_lt_toNNReal_iff_of_nonneg, coe_nnnorm, Complex.norm_eq_abs, NNReal.coe_pow, Real.coe_toNNReal',
  max_eq_left, sub_nonneg] at this
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ↑Complex.abs (eval (↑q) (cyclotomic n ℂ)) < max (q + 1) 0 ^ φ n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
[PROOFSTEP]
convert this using 2
[GOAL]
case h.e'_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ↑Complex.abs (eval (↑q) (cyclotomic n ℂ)) < max (q + 1) 0 ^ φ n
⊢ eval q (cyclotomic n ℝ) = ↑Complex.abs (eval (↑q) (cyclotomic n ℂ))
[PROOFSTEP]
erw [cyclotomic.eval_apply q n (algebraMap ℝ ℂ), eq_comm]
[GOAL]
case h.e'_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ↑Complex.abs (eval (↑q) (cyclotomic n ℂ)) < max (q + 1) 0 ^ φ n
⊢ ↑Complex.abs (↑(algebraMap ℝ ℂ) (eval q (cyclotomic n ℝ))) = eval q (cyclotomic n ℝ)
[PROOFSTEP]
simp [cyclotomic_nonneg n hq'.le]
[GOAL]
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ↑Complex.abs (eval (↑q) (cyclotomic n ℂ)) < max (q + 1) 0 ^ φ n
⊢ q + 1 = max (q + 1) 0
[PROOFSTEP]
rw [eq_comm, max_eq_left_iff]
[GOAL]
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ↑Complex.abs (eval (↑q) (cyclotomic n ℂ)) < max (q + 1) 0 ^ φ n
⊢ 0 ≤ q + 1
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ (_ : ¬‖eval (↑q) (cyclotomic n ℂ)‖₊ = 0) <
    Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0) ^ φ n
[PROOFSTEP]
simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub, nnnorm_prod, Units.mk0_prod]
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∏ b in attach (primitiveRoots n ℂ), Units.mk0 ‖↑q - ↑b‖₊ (_ : ‖↑q - ↑b‖₊ = 0 → False) <
    Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0) ^ φ n
[PROOFSTEP]
convert Finset.prod_lt_prod' (M := NNRealˣ) _ _
[GOAL]
case h.e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0) ^ φ n =
    ∏ i in attach (primitiveRoots n ℂ), ?convert_3 i
case convert_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ { x // x ∈ primitiveRoots n ℂ } → NNRealˣ
case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ (i : { x // x ∈ primitiveRoots n ℂ }),
    i ∈ attach (primitiveRoots n ℂ) → Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False) ≤ ?convert_3 i
case convert_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i, i ∈ attach (primitiveRoots n ℂ) ∧ Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False) < ?convert_3 i
[PROOFSTEP]
swap
[GOAL]
case convert_3
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ { x // x ∈ primitiveRoots n ℂ } → NNRealˣ
[PROOFSTEP]
exact fun _ => Units.mk0 (Real.toNNReal (q + 1)) (by simp; linarith only [hq'])
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x✝ : { x // x ∈ primitiveRoots n ℂ }
⊢ Real.toNNReal (q + 1) ≠ 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x✝ : { x // x ∈ primitiveRoots n ℂ }
⊢ 0 < q + 1
[PROOFSTEP]
linarith only [hq']
[GOAL]
case h.e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0) ^ φ n =
    ∏ i in attach (primitiveRoots n ℂ), Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0)
[PROOFSTEP]
simp [Complex.card_primitiveRoots]
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ (i : { x // x ∈ primitiveRoots n ℂ }),
    i ∈ attach (primitiveRoots n ℂ) →
      Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False) ≤
        Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0)
[PROOFSTEP]
simp only [Subtype.coe_mk, Finset.mem_attach, forall_true_left, Subtype.forall, ← Units.val_le_val, ← NNReal.coe_le_coe,
  Complex.abs.nonneg, hq'.le, Units.val_mk0, Real.coe_toNNReal, coe_nnnorm, Complex.norm_eq_abs, max_le_iff]
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∀ (a : ℂ), a ∈ primitiveRoots n ℂ → ↑Complex.abs (↑q - a) ≤ ↑(Real.toNNReal (q + 1))
[PROOFSTEP]
intro x hx
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
⊢ ↑Complex.abs (↑q - x) ≤ ↑(Real.toNNReal (q + 1))
[PROOFSTEP]
have : Complex.abs _ ≤ _ := hfor x hx
[GOAL]
case convert_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
this : ↑Complex.abs (↑q - x) ≤ q + 1
⊢ ↑Complex.abs (↑q - x) ≤ ↑(Real.toNNReal (q + 1))
[PROOFSTEP]
simp [this]
[GOAL]
case convert_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ i,
    i ∈ attach (primitiveRoots n ℂ) ∧
      Units.mk0 ‖↑q - ↑i‖₊ (_ : ‖↑q - ↑i‖₊ = 0 → False) <
        Units.mk0 (Real.toNNReal (q + 1)) (_ : Real.toNNReal (q + 1) ≠ 0)
[PROOFSTEP]
simp only [Subtype.coe_mk, Finset.mem_attach, exists_true_left, Subtype.exists, ← NNReal.coe_lt_coe, ← Units.val_lt_val,
  Units.val_mk0 _, coe_nnnorm]
[GOAL]
case convert_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ', ζ' ∈ primitiveRoots n ℂ ∧ ‖↑q - ζ'‖ < q + 1
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ ∃ a h, True ∧ ‖↑q - a‖ < ↑(Real.toNNReal (q + 1))
[PROOFSTEP]
obtain ⟨ζ, hζ, hhζ : Complex.abs _ < _⟩ := hex
[GOAL]
case convert_6.intro.intro
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ✝ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ✝ : IsPrimitiveRoot ζ✝ n
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
ζ : ℂ
hζ : ζ ∈ primitiveRoots n ℂ
hhζ : ↑Complex.abs (↑q - ζ) < q + 1
⊢ ∃ a h, True ∧ ‖↑q - a‖ < ↑(Real.toNNReal (q + 1))
[PROOFSTEP]
exact ⟨ζ, hζ, by simp [hhζ]⟩
[GOAL]
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ (ζ' : ℂ), ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1
ζ✝ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ✝ : IsPrimitiveRoot ζ✝ n
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
ζ : ℂ
hζ : ζ ∈ primitiveRoots n ℂ
hhζ : ↑Complex.abs (↑q - ζ) < q + 1
⊢ True ∧ ‖↑q - ζ‖ < ↑(Real.toNNReal (q + 1))
[PROOFSTEP]
simp [hhζ]
[GOAL]
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 0 ℝ) ≤ (q + 1) ^ φ 0
[PROOFSTEP]
simp
[GOAL]
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 1 ℝ) ≤ (q + 1) ^ φ 1
[PROOFSTEP]
simp [add_assoc, add_nonneg, zero_le_one]
[GOAL]
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 2 ℝ) ≤ (q + 1) ^ φ 2
[PROOFSTEP]
simp
[GOAL]
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
⊢ (q - 1) ^ φ n < Int.natAbs (eval (↑q) (cyclotomic n ℤ))
[PROOFSTEP]
rcases hq.lt_or_lt.imp_left Nat.lt_one_iff.mp with (rfl | hq')
[GOAL]
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (0 - 1) ^ φ n < Int.natAbs (eval (↑0) (cyclotomic n ℤ))
[PROOFSTEP]
rw [zero_tsub, zero_pow (Nat.totient_pos (pos_of_gt hn')), pos_iff_ne_zero, Int.natAbs_ne_zero, Nat.cast_zero, ←
  coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hn']
[GOAL]
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < Int.natAbs (eval (↑q) (cyclotomic n ℤ))
[PROOFSTEP]
rw [← @Nat.cast_lt ℝ, Nat.cast_pow, Nat.cast_sub hq'.le, Nat.cast_one, Int.cast_natAbs]
[GOAL]
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (↑q - 1) ^ φ n < ↑|eval (↑q) (cyclotomic n ℤ)|
[PROOFSTEP]
refine' (sub_one_pow_totient_lt_cyclotomic_eval hn' (Nat.one_lt_cast.2 hq')).trans_le _
[GOAL]
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ eval (↑q) (cyclotomic n ℝ) ≤ ↑|eval (↑q) (cyclotomic n ℤ)|
[PROOFSTEP]
convert (cyclotomic.eval_apply (q : ℤ) n (algebraMap ℤ ℝ)).trans_le (le_abs_self _)
[GOAL]
case h.e'_4
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ ↑|eval (↑q) (cyclotomic n ℤ)| = |↑(algebraMap ℤ ℝ) (eval (↑q) (cyclotomic n ℤ))|
[PROOFSTEP]
simp