Last week, Matt Springer wrote a nice essay on trigonometric orthogonality. Proving orthogonality requires some identities that I have forgotten before.
This in turn lead me to try to remember where that came from.
My previous entry demonstrated that we could replace the product of the sines of any two angles with a sum of cosines depending on the sum and difference of the angles, and likewise for the other products. Alas, the proof this depends on knowing the correct formula for the cosine of the sum of an angle, which I didn't demonstrate there.
In practice, it turns out to be a little easier to start from the formula for the difference of two angles - we can then demonstrate the formula for the sum by substituting a negative angle and grinding out the correct changes in sign.

We begin with a large angle a and a smaller angle b, and we want to calculate the cosine of the difference. We'll take a page from M. Descartes, and plot the two angles on a unit circle. The thick black line segment will be the key; how long is it? To avoid the clutter of square roots, we calculate the square of the length as follows:
L^2
= (cos(a)-cos(b))^2 + (sin(a)-sin(b))^2
= cos(a)cos(a) - 2cos(a)cos(b) + cos(b)cos(b) + sin(a)sin(a) - 2sin(a)sin(b) + sin(b)sin(b)
= cos(a)cos(a) + sin(a)sin(a) + cos(b)cos(b) + sin(b)sin(b) - 2 (cos(a)cos(b) + sin(a)sin(b))
= 1 + 1 - 2 (cos(a)cos(b) + sin(a)sin(b))
= 2 [ 1 - (cos(a)cos(b) + sin(a)sin(b)) ]
Now, rotating the unit circle around doesn't change any of the lengths, it just changes all of the angles by the same amount. So we rotate all of the angles by -b....
L^2
= 2 [ 1 - (cos(a)cos(b) + sin(a)sin(b)) ]
= 2 [ 1 - (cos(a-b)cos(b-b) + sin(a-b)sin(b-b)) ]
= 2 [ 1 - (cos(a-b)cos(0) + sin(a-b)sin(0)) ]
= 2 [ 1 - (cos(a-b)(1) + sin(a-b)(0)) ]
= 2 [ 1 - cos(a-b) ]
Applying the appropriate algebra, we get
cos(a-b)
= cos(a)cos(b) + sin(a)sin(b)
And as promised
cos(a+b)
= cos(a)cos(b) - sin(a)sin(b)