English
4 cos^2(π/5) - 2 cos(π/5) - 1 = 0.
Русский
4 cos^2(π/5) - 2 cos(π/5) - 1 = 0.
LaTeX
$$$4 \cos^2\left(\\frac{\\pi}{5}\\right) - 2 \cos\left(\\frac{\\pi}{5}\\right) - 1 = 0$$$
Lean4
theorem quadratic_root_cos_pi_div_five :
letI c := cos (π / 5)
4 * c ^ 2 - 2 * c - 1 = 0 :=
by
set θ := π / 5 with hθ
set c := cos θ
set s := sin θ
suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]
have hs : s ≠ 0 := by
rw [ne_eq, sin_eq_zero_iff, hθ]
push_neg
intro n hn
replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
omega
suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this
calc
s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
_ = sin (2 * θ) := by rw [sin_two_mul]
_ = sin (π - 2 * θ) := by rw [sin_pi_sub]
_ = sin (2 * θ + θ) := by congr; linarith
_ = sin (2 * θ) * c + cos (2 * θ) * s := (sin_add (2 * θ) θ)
_ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
_ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
_ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
_ = s * (4 * c ^ 2 - 1) := by linarith
