Fungrim home page

Fungrim entry: 1d730a

atan2 ⁣(y1,x1)atan2 ⁣(y2,x2)=atan2 ⁣(y1x2y2x1,x1x2+y1y2)\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:x1Randx2Randy1Randy2Randatan2 ⁣(y1,x1)atan2 ⁣(y2,x2)(π,π]andnot(x1=y1=0)andnot(x2=y2=0){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
Atan2atan2 ⁣(y,x)\operatorname{atan2}\!\left(y, x\right) Two-argument inverse tangent
RRR\mathbb{R} Real numbers
OpenClosedInterval(a,b]\left(a, b\right] Open-closed interval
ConstPiπ\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(ConstPi), ConstPi)), 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.

2019-06-18 07:49:59.356594 UTC