arctan_add_eq_sub_pi — Mathlib

English

If 1 < xy and x < 0, then arctan x + arctan y = arctan((x+y)/(1-xy)) − π.

Русский

Если 1 < xy и x < 0, то arctan x + arctan y = arctan((x+y)/(1-xy)) − π.

LaTeX

$$$1 < xy \\land x < 0 \\Rightarrow \\arctan x + \\arctan y = \\arctan\\left(\\\\frac{x+y}{1-xy}\\\\right) - π.$$$

Lean4

theorem arctan_add_eq_sub_pi (h : 1 < x * y) (hx : x < 0) : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π :=
  by
  rw [← neg_mul_neg] at h
  have k := arctan_add_eq_add_pi h (neg_pos.mpr hx)
  rw [show _ / _ = -((x + y) / (1 - x * y)) by ring, ← neg_inj] at k
  simp only [arctan_neg, neg_add, neg_neg, ← sub_eq_add_neg _ π] at k
  exact k

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