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)))))