cos_sub_cos — Mathlib

English

For all complex x,y, cos x − cos y = −2 sin((x + y)/2) sin((x − y)/2).

Русский

Для любых комплексных x и y верно: cos x − cos y = −2 sin((x + y)/2) sin((x − y)/2).

LaTeX

$$$ \cos x - \cos y = -2 \sin\left(\frac{x + y}{2}\right) \sin\left(\frac{x - y}{2}\right).$$$

Lean4

theorem cos_sub_cos : cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2) :=
  by
  have s1 := cos_add ((x + y) / 2) ((x - y) / 2)
  have s2 := cos_sub ((x + y) / 2) ((x - y) / 2)
  rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1
  rw [div_sub_div_same, ← sub_add, add_sub_cancel_left, add_self_div_two] at s2
  rw [s1, s2]
  ring

Похожие утверждения