English
For all complex x,y, cos x + cos y = 2 cos((x + y)/2) cos((x − y)/2).
Русский
Для любых комплексных x и y верно: cos x + cos y = 2 cos((x + y)/2) cos((x − y)/2).
LaTeX
$$$ \cos x + \cos y = 2 \cos\left(\frac{x + y}{2}\right) \cos\left(\frac{x - y}{2}\right).$$$
Lean4
theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) :=
by
calc
cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
_ =
cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
(cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
?_
_ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
· congr <;> field_simp <;> ring
· rw [cos_add, cos_sub]
ring
