arctan_add_eq_add_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_add_pi (h : 1 < x * y) (hx : 0 < x) : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π :=
  by
  have hy : 0 < y := by
    have := mul_pos_iff.mp (zero_lt_one.trans h)
    simpa [hx, hx.asymm]
  have k := arctan_add (mul_inv x y ▸ inv_lt_one_of_one_lt₀ h)
  rw [arctan_inv_of_pos hx, arctan_inv_of_pos hy, show _ + _ = π - (arctan x + arctan y) by ring, sub_eq_iff_eq_add, ←
    sub_eq_iff_eq_add', sub_eq_add_neg, ← arctan_neg, add_comm] at k
  grind

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