Proof of Addition Formulas for Sine and Cosine

Routine facts are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity); results on real and imaginary parts are read for the current complex numbers by The Earlier and the New Versions of the Definitions of the Natural Numbers, the Complex Numbers, the Conjugate and the Modulus Agree, and the Two Versions of Real Correspond (ii).

Both formulas are obtained by evaluating the functional equation of the exponential on the imaginary axis and comparing real and imaginary parts.

The functional equation. Let $\exp$ be the complex exponential function. Since $i(a+x)=ia+ix$, the functional equation The Complex Exponential: the Functional Equation, Conjugates, Real Arguments and the Modulus (ii), applied with $z=ia$ and $w=ix$, gives

$$\exp\bigl(i(a+x)\bigr)=\exp(ia)\,\exp(ix).$$

Both sides in canonical form. By Euler's formula Euler's Formula: the Complex Exponential on the Imaginary Axis, Its Modulus and Its Conjugate (i), applied with $t=a+x$, the left side is $\cos(a+x)+i\sin(a+x)$. On the right side, Euler's formula applied with $t=a$ and with $t=x$ writes the two factors as $\cos a+i\sin a$ and $\cos x+i\sin x$. Their product is computed by the rule for multiplying complex numbers written as $p+qi$ with $p$ and $q$ real (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (vii)):

$$(\cos a+i\sin a)(\cos x+i\sin x)=(\cos a\cos x-\sin a\sin x)+(\sin a\cos x+\cos a\sin x)\,i .$$

Comparison. We have thus written $\exp\bigl(i(a+x)\bigr)$ in two ways,

$$\cos(a+x)+\sin(a+x)\,i=(\cos a\cos x-\sin a\sin x)+(\sin a\cos x+\cos a\sin x)\,i ,$$

and the four numbers $\cos(a+x)$, $\sin(a+x)$, $\cos a\cos x-\sin a\sin x$ and $\sin a\cos x+\cos a\sin x$ are real. By the uniqueness of the real and imaginary parts (Real and Imaginary Parts of a Complex Number (i)), the two sides have the same real part and the same imaginary part. Equating the real parts gives (i), and equating the imaginary parts gives (ii).