Fungrim entry: a020e9

\operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) = \operatorname{atan2}\!\left({y}_{1} {x}_{2} + {y}_{2} {x}_{1}, {x}_{1} {x}_{2} - {y}_{1} {y}_{2}\right)

Assumptions:

{x}_{1} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; {x}_{2} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; {y}_{1} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; {y}_{2} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; \operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) \in \left(-\pi, \pi\right] \;\mathbin{\operatorname{and}}\; \operatorname{not} \left({x}_{1} = {y}_{1} = 0\right) \;\mathbin{\operatorname{and}}\; \operatorname{not} \left({x}_{2} = {y}_{2} = 0\right)

TeX:

\operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) = \operatorname{atan2}\!\left({y}_{1} {x}_{2} + {y}_{2} {x}_{1}, {x}_{1} {x}_{2} - {y}_{1} {y}_{2}\right)

{x}_{1} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; {x}_{2} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; {y}_{1} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; {y}_{2} \in \mathbb{R} \;\mathbin{\operatorname{and}}\; \operatorname{atan2}\!\left({y}_{1}, {x}_{1}\right) + \operatorname{atan2}\!\left({y}_{2}, {x}_{2}\right) \in \left(-\pi, \pi\right] \;\mathbin{\operatorname{and}}\;  \operatorname{not} \left({x}_{1} = {y}_{1} = 0\right) \;\mathbin{\operatorname{and}}\;  \operatorname{not} \left({x}_{2} = {y}_{2} = 0\right)

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`RR`	$\mathbb{R}$	Real numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Pi`	$\pi$	The constant pi (3.14...)

Source code for this entry:

Entry(ID("a020e9"),
    Formula(Equal(Add(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), Atan2(Add(Mul(Subscript(y, 1), Subscript(x, 2)), Mul(Subscript(y, 2), Subscript(x, 1))), Sub(Mul(Subscript(x, 1), Subscript(x, 2)), Mul(Subscript(y, 1), Subscript(y, 2)))))),
    Variables(x, y),
    Assumptions(And(Element(Subscript(x, 1), RR), Element(Subscript(x, 2), RR), Element(Subscript(y, 1), RR), Element(Subscript(y, 2), RR), Element(Add(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), OpenClosedInterval(Neg(Pi), Pi)), Not(Equal(Subscript(x, 1), Subscript(y, 1), 0)), Not(Equal(Subscript(x, 2), Subscript(y, 2), 0)))))

Topics using this entry

Inverse tangent