Fungrim home page

Fungrim entry: b65d19

Im ⁣(atan ⁣(x+yi))=14log ⁣(x2+(1+y)2x2+(1y)2)\operatorname{Im}\!\left(\operatorname{atan}\!\left(x + y i\right)\right) = \frac{1}{4} \log\!\left(\frac{{x}^{2} + {\left(1 + y\right)}^{2}}{{x}^{2} + {\left(1 - y\right)}^{2}}\right)
Assumptions:xRandyRandx+yi{i,i}x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \notin \left\{-i, i\right\}
TeX:
\operatorname{Im}\!\left(\operatorname{atan}\!\left(x + y i\right)\right) = \frac{1}{4} \log\!\left(\frac{{x}^{2} + {\left(1 + y\right)}^{2}}{{x}^{2} + {\left(1 - y\right)}^{2}}\right)

x \in \mathbb{R} \,\mathbin{\operatorname{and}}\, y \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x + y i \notin \left\{-i, i\right\}
Definitions:
Fungrim symbol Notation Short description
ImIm ⁣(z)\operatorname{Im}\!\left(z\right) Imaginary part
Atanatan ⁣(z)\operatorname{atan}\!\left(z\right) Inverse tangent
ConstIii Imaginary unit
Loglog ⁣(z)\log\!\left(z\right) Natural logarithm
Powab{a}^{b} Power
RRR\mathbb{R} Real numbers
Source code for this entry:
Entry(ID("b65d19"),
    Formula(Equal(Im(Atan(Add(x, Mul(y, ConstI)))), Mul(Div(1, 4), Log(Div(Add(Pow(x, 2), Pow(Add(1, y), 2)), Add(Pow(x, 2), Pow(Sub(1, y), 2))))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR), NotElement(Add(x, Mul(y, ConstI)), Set(Neg(ConstI), ConstI)))))

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