Proof of The Pythagorean Identity for Sine and Cosine

Routine facts are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity); results on real and imaginary parts and moduli 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) and 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 (iv).

Both assertions come from reading $\cos x$ and $\sin x$ as the coordinates of a point on the unit circle. Let $\exp$ be the complex exponential function and let $z=\exp(ix)$. By the definitions of the cosine and the sine (The Real Sine and Cosine Functions (i), The Real Sine and Cosine Functions (ii)), $\operatorname{Re}z=\cos x$ and $\operatorname{Im}z=\sin x$; and $|z|=1$, by Euler's Formula: the Complex Exponential on the Imaginary Axis, Its Modulus and Its Conjugate (ii) applied with $t=x$.

The identity. For every complex number, the square of its modulus is the sum of the squares of its real and imaginary parts, by Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums (iii). Applied to $z$, this gives

$$(\cos x)^{2}+(\sin x)^{2}=(\operatorname{Re}z)^{2}+(\operatorname{Im}z)^{2}=|z|^{2}=1 ,$$

which is (i).

Bounds. Neither the real nor the imaginary part of a complex number exceeds its modulus in absolute value, by Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums (vi). Applied to $z$, this gives

$$|\cos x|=|\operatorname{Re}z|\le|z|=1,\qquad |\sin x|=|\operatorname{Im}z|\le|z|=1,$$

which is (ii).