# Fungrim entry: 14f8c2

$\operatorname{atan}\!\left(2 z\right) = \operatorname{atan}(z) + \operatorname{atan}\!\left(\frac{z}{1 + 2 {z}^{2}}\right)$
Assumptions:$z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \operatorname{not} \left(\operatorname{Re}(z) = 0 \;\mathbin{\operatorname{and}}\; \left|\operatorname{Im}(z)\right| \in \left[\frac{\sqrt{2}}{2}, 1\right]\right)$
TeX:
\operatorname{atan}\!\left(2 z\right) = \operatorname{atan}(z) + \operatorname{atan}\!\left(\frac{z}{1 + 2 {z}^{2}}\right)

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\;  \operatorname{not} \left(\operatorname{Re}(z) = 0 \;\mathbin{\operatorname{and}}\; \left|\operatorname{Im}(z)\right| \in \left[\frac{\sqrt{2}}{2}, 1\right]\right)
Definitions:
Fungrim symbol Notation Short description
Atan$\operatorname{atan}(z)$ Inverse tangent
Pow${a}^{b}$ Power
CC$\mathbb{C}$ Complex numbers
Re$\operatorname{Re}(z)$ Real part
Abs$\left|z\right|$ Absolute value
Im$\operatorname{Im}(z)$ Imaginary part
ClosedInterval$\left[a, b\right]$ Closed interval
Sqrt$\sqrt{z}$ Principal square root
Source code for this entry:
Entry(ID("14f8c2"),
Assumptions(And(Element(z, CC), Not(And(Equal(Re(z), 0), Element(Abs(Im(z)), ClosedInterval(Div(Sqrt(2), 2), 1)))))))