The cosine rule

I realized that I had completely forgotten how the cosine rule was proved at school. So I found myself thinking about the design of a proof. In the usual terminology the cosine rule states

(0)	`c`² = `a`² + `b`² - 2·`a`·`b`·cos.`γ`

A simple proof observes

(1)	`c` = `a`·cos.`β` + `b`·cos.`α`	and
(2)	0 = `a`·sin.`β` - `b`·sin.`α`

(the latter is the rule of sines; it follows from a·c·sin.β = b·c·sin.α, both sides equalling twice the area of the triangle). Squaring both sides of (1) and (2) and adding yields (0) —using

(3)	cos.`γ` = - cos.(`α`+`β`)	since `α`+`β`+`γ` = π,
(4)	cos.(`α`+`β`) = cos.`α`·cos.`β` - sin.`α`·sin.`β`

So far so good. Then I tried to derive this proof in a more orderly fashion. So I started with the right-hand side. Application of (3) for symmetry's sake yields

a² + b² + 2·a·b·cos.(α+β)

and since (4) is the only thing we know about cos.(α+β), its application readily yields

a² + b² + 2·a·b·( cos.α·cos.β - sin.α·sin.β )

Just remembering "sin² + cos² = 1" suffices to make you try to rewrite this as a sum of squares. But there is a snag! The expression being symmetric in α and β, it also admits the decomposition

(a·cos.α + b·cos.β)² + (a·sin.α - b·sin.β)²

a decomposition that leads nowhere. An "honest" derivation considers both alternatives, at least as long as we don't wish to pull (1) or (2) out of the magician's hat.

The alternative is not to start with the right-hand side of (0) but with (0) and (1). Squaring the latter, subtracting the result from (0) and simplifying reduces the proof obligation to the rule of sines:

	(`a`·sin.`β`)² + (`b`·sin.`α`)² - 2·`a`·`b`·(cos.`γ` + cos.`α`·cos.`β`)

= { (3) }
	(`a`·sin.`β`)² + (`b`·sin.`α`)² + 2·`a`·`b`·(cos.(`α`+`β`) - cos.`α`·cos.`β`)
= { (4) }
	(`a`·sin.`β`)² + (`b`·sin.`α`)² - 2·`a`·`b`·sin.`α`·sin.`β`
= { algebra }
	(`a`·sin.`β` - `b`·sin.`α`)²
= { rule of sines }
	0.

This is a proof of the type "there is really nothing else you can do", but for that, we had to start with (1) so as to be steered away from the barren decomposition.

Austin, 4 September 1986

prof. dr. Edsger W. Dijkstra
Department of Computer Sciences
The University of Texas at Austin
Austin, TX 78712-1188
USA

Transcribed by Martijn van der Veen.

Revised Fri, 28 May 2010.