Assumptions:
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 |
---|---|---|
Im | Imaginary part | |
Atan | Inverse tangent | |
ConstI | Imaginary unit | |
Log | Natural logarithm | |
Pow | Power | |
RR | 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)))))