ThmDex – An index of mathematical definitions, results, and conjectures.
Fundamental theorem of complex trigonometry
Formulation 0
Let $\sin$ be the D164: Standard complex sine function.
Let $\cos$ be the D165: Standard complex cosine function.
Let $z \in \mathbb{C}$ be a D1207: Complex number.
Then \begin{equation} \sin^2 z + \cos^2 z = 1 \end{equation}
Subresults
R5127: Fundamental theorem of real trigonometry
Proofs
Proof 0
Let $\sin$ be the D164: Standard complex sine function.
Let $\cos$ be the D165: Standard complex cosine function.
Let $z \in \mathbb{C}$ be a D1207: Complex number.
Using results
(i) R5128: Standard complex sine function expressed in terms of complex exponential function
(ii) R5129: Standard complex cosine function expressed in terms of complex exponential function
(iii) R5119: Binary homomorphism property of standard natural complex exponential function

we have \begin{equation} \begin{split} \cos^2 z + \sin^2 z & = \left( \frac{e^{i z} + e^{- i z}}{2} \right)^2 + \left( \frac{e^{i z} - e^{- i z}}{2 i} \right)^2 \\ & = \frac{1}{4} \left( e^{i z} e^{i z} + 2 e^{- i z} e^{i z} + e^{- i z} e^{- i z} \right)^2 - \frac{1}{4} \left( e^{i z} e^{i z} - 2 e^{- i z} e^{i z} + e^{- i z} e^{- i z} \right)^2 \\ & = \frac{1}{4} \left( e^{2 i z} + 2 + e^{- 2 i z} \right)^2 - \frac{1}{4} \left( e^{2 i z} - 2 + e^{- 2 i z} \right)^2 \\ & = \frac{1}{4} e^{2 i z} + \frac{1}{2} + \frac{1}{4} e^{- 2 i z} - \frac{1}{4} e^{2 i z} + \frac{1}{2} - \frac{1}{4} e^{- 2 i z} \\ & = \frac{1}{2} + \frac{1}{2} \\ & = 1 \end{split} \end{equation} $\square$