Let $\cos$ be the D1927: Standard real cosine function.
Let $\sin$ be the D1931: Standard real sine function.
Let $x \in \mathbb{R}$ be a D993: Real number.
Let $n \in \mathbb{Z}$ be a D995: Integer.
Let $\sin$ be the D1931: Standard real sine function.
Let $x \in \mathbb{R}$ be a D993: Real number.
Let $n \in \mathbb{Z}$ be a D995: Integer.
Then
\begin{equation}
\left( \cos(x) + i \sin(x) \right)^n
= \cos (n x) + i \sin (n x)
\end{equation}