Proofs of $\cos(x+y) = \cos x\cos y - \sin x \sin y$

Define $\sin x $ and $\cos x$ via their infinite series: $$ \sin x = \sum_n (-1)^{n}\frac{x^{2n+1}}{(2n+1)!}, \qquad \cos x = \sum_n (-1)^n \frac{x^{2n}}{(2n)!}. $$ Is there a short, clever proof that $\cos(x+y) = \cos x \cos y - \sin x \sin y$ for all real $x,y$? I can prove it using product series, or by showing that both sides (with $y$ fixed) are solutions of $f''(x) = -f(x)$, $f(0) = \cos y$, $f'(0) = - \sin y$. Does anyone know other (preferably slick!) proofs?

One way is to use the fact that $$\cos(\theta) = \dfrac{e^{i \theta}+e^{-i \theta}}2$$ $$\cos(x+y) = \dfrac{e^{i(x+y)}+e^{-i(x+y)}}2 = \left(\dfrac{e^{ix}+e^{-ix}}2 \right) \left(\dfrac{e^{iy}+e^{-iy}}2\right) - \left(\dfrac{e^{ix}-e^{-ix}}{2i} \right) \left(\dfrac{e^{iy}-e^{-iy}}{2i}\right)$$

New answer to an old question. This one, maybe the slickiest of them all, is due to Erhard Schmidt.
Define $$f(t)=\cos(x+y-t)\cos(t)-\sin(x+y-t)\sin(t).$$ Verify $f'(t)=0$, hence $f$ is constant. Now the desired angle sum identity follows from $f(0)=f(y)$

This was addressed in the question already. I leave it so that the method is fully explained.

LEMMA Let $f$ be a function with second derivative everywhere such that $f''+f=0$ and $f'(0)=0$; $f(0)=0$. Then $f$ is identically zero everywhere.

P We have that $$f''+f=0$$ Then $$f'f''+ff'=0$$ or $$(f')^2+f^2=C$$

But the initial conditions force $f'^2+f^2=0$ everywhere, which means $f\equiv 0$. $\blacktriangle$.

PROP Let $f$ be a function with second derivative everywhere such that $f''+f=0$, and $f'(0)=a$, $f(0)=b$. Then $$f=a\sin+b\cos $$

P Let $g=f-a\sin+b\cos$. Then $g''+g=0$ and $g'(0)=0$, $g(0)=0$. The lemma implies $g\equiv 0$, so that $f=a\sin+b\cos$. $\blacktriangle$.

Differentiate with respect to one variable and use the uniqueness of the solution of a second degree ODE with initial conditions.

That is, your cosine on the left vetifies $$f''+f=0$$ and $f'(0)=–\sin y$, $f''(0)=\cos y$. Then it must coincide with the unique solution $$f'(0) \sin+f(0)\cos$$