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:xR  and  yR  and  x+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\}
\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\}
Fungrim symbol Notation Short description
ImIm(z)\operatorname{Im}(z) Imaginary part
Atanatan(z)\operatorname{atan}(z) Inverse tangent
ConstIii Imaginary unit
Loglog(z)\log(z) Natural logarithm
Powab{a}^{b} Power
RRR\mathbb{R} Real numbers
Source code for this entry:
    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.

2021-03-15 19:12:00.328586 UTC