# Fungrim entry: 1d730a

$\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("1d730a"),
Formula(Equal(Sub(Atan2(Subscript(y, 1), Subscript(x, 1)), Atan2(Subscript(y, 2), Subscript(x, 2))), Atan2(Sub(Mul(Subscript(y, 1), Subscript(x, 2)), Mul(Subscript(y, 2), Subscript(x, 1))), Add(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(Sub(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

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC