Quintuple-Angle Formula

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Quintuple-Angle Formula
[blueprint]

$\cos(5x) = 16\cos^5 x - 20\cos^3 x + 5\cos x.$

theorem cos_five_mul (x : ℝ) :
    Real.cos (5 * x) = 16 * Real.cos x ^ 5 - 20 * Real.cos x ^ 3 + 5 * Real.cos x := by
Proof ▼ 


  have h1 : (5 : ℝ) * x = 2 * x + 3 * x := by ring
  rw [h1, Real.cos_add, Real.cos_two_mul, Real.sin_two_mul, Real.cos_three_mul,
      Real.sin_three_mul]
  have h_sin2 : Real.sin x ^ 2 = 1 - Real.cos x ^ 2 := by
    have := Real.sin_sq_add_cos_sq x; linarith
  have h_sin3 : Real.sin x ^ 3 = Real.sin x * (1 - Real.cos x ^ 2) := by
    rw [pow_succ, h_sin2]; ring
  rw [h_sin3]
  calc (2 * Real.cos x ^ 2 - 1) * (4 * Real.cos x ^ 3 - 3 * Real.cos x) -
        2 * Real.sin x * Real.cos x * (3 * Real.sin x -
        4 * (Real.sin x * (1 - Real.cos x ^ 2)))
      = (2 * Real.cos x ^ 2 - 1) * (4 * Real.cos x ^ 3 - 3 * Real.cos x) -
        2 * Real.sin x ^ 2 * Real.cos x * (4 * Real.cos x ^ 2 - 1) := by ring
    _ = (2 * Real.cos x ^ 2 - 1) * (4 * Real.cos x ^ 3 - 3 * Real.cos x) -
        2 * (1 - Real.cos x ^ 2) * Real.cos x * (4 * Real.cos x ^ 2 - 1) := by rw [h_sin2]
    _ = 16 * Real.cos x ^ 5 - 20 * Real.cos x ^ 3 + 5 * Real.cos x := by ring

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