Angle addition formulas

Statement

For all real numbers $x$ and $y$, $$\sin(x + y) = \sin x \cos y + \cos x \sin y,$$ $$\cos(x + y) = \cos x \cos y - \sin x \sin y.$$

Remarks

One proof multiplies the power series with the Cauchy product and uses the binomial theorem. Another proof fixes $y$ and shows that the difference of the two sides solves $f'' = -f$ with $f(0) = f'(0) = 0$. With $y = x$, they give $\sin 2x = 2 \sin x \cos x$ and $\cos 2x = \cos^2 x - \sin^2 x$. Mathlib states them as Real.sin_add and Real.cos_add.

Explanations

L1 human

These formulas compute the sine and cosine of a sum of two angles from the sines and cosines of the angles. They are the most important trigonometric identities.