Nonvanishing Cosine at Odd Roots

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Nonvanishing Cosine at Odd Roots
[blueprint]

For odd $N \ge 5$ and $0 < k < N$, $\cos(2\pi k/N) \ne 0.$

theorem cos_two_pi_k_div_odd_N_ne_zero (N k : ℕ) (hN_odd : Odd N) (hN_ge : N ≥ 5)
    (_hk_pos : 0 < k) (hk_lt : k < N) :
    Real.cos (2 * Real.pi * k / N) ≠ 0 := by
Proof ▼ 


  intro h
  rw [Real.cos_eq_zero_iff] at h
  obtain ⟨m, hm⟩ := h
  have eq_real : (4 : ℝ) * k = N * (2 * m + 1) := by
    have h3 := congr_arg (· * (2 * N / Real.pi)) hm
    field_simp at h3; linarith
  obtain ⟨n, rfl⟩ := hN_odd
  have eq_int : (4 * k : ℤ) = (2 * (n : ℤ) + 1) * (2 * m + 1) := by
    have h1 : (4 * k : ℝ) = ((2 * n + 1 : ℕ) : ℝ) * (2 * (m : ℤ) + 1) := by
      convert eq_real using 2
    have h2 : ((2 * n + 1 : ℕ) : ℝ) = ((2 * (n : ℤ) + 1) : ℝ) := by norm_cast
    have h3 : (4 * k : ℝ) = ((2 * (n : ℤ) + 1) * (2 * m + 1) : ℤ) := by
      calc (4 * k : ℝ) = ((2 * n + 1 : ℕ) : ℝ) * (2 * (m : ℤ) + 1) := h1
        _ = ((2 * (n : ℤ) + 1) : ℝ) * (2 * m + 1) := by rw [h2]
        _ = ((2 * (n : ℤ) + 1) * (2 * m + 1) : ℤ) := by norm_cast
    exact_mod_cast h3
  have h_expand : (2 * (n : ℤ) + 1) * (2 * m + 1) = 2 * (2 * n * m + n + m) + 1 := by ring
  rw [h_expand] at eq_int
  have h_even : Even (4 * k : ℤ) := ⟨2 * k, by ring⟩
  have h_odd : Odd (2 * (2 * (n : ℤ) * m + n + m) + 1) := ⟨2 * n * m + n + m, rfl⟩
  rw [← eq_int] at h_odd
  exact Int.not_even_iff_odd.mpr h_odd h_even

Dependencies (uses)

None

Dependents (used by)

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms