sin_sub_sin — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sin_sub_sin : sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2) :=
  by
  have s1 := sin_add ((x + y) / 2) ((x - y) / 2)
  have s2 := sin_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

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