ThmDex – An index of mathematical definitions, results, and conjectures.
P3503
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$