Theorem: Spherical Law of Cosines

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Then:
:$\cos a = \cos b \cos c + \sin b \sin c \cos A$

Proof:
:500px
Let $A$, $B$ and $C$ be the vertices of a spherical triangle on the surface of a sphere $S$.
By definition of a spherical triangle, $AB$, $BC$ and $AC$ are arcs of great circles on $S$.
By definition of a great circle, the center of each of these great circles is $O$.
Let $O$ be joined to each of $A$, $B$ and $C$.
Let $P$ be an arbitrary point on $OC$.
Construct $PQ$ perpendicular to $OA$ meeting $OA$ at $Q$.
Construct $PR$ perpendicular to $OB$ meeting $OB$ at $R$.
In the plane $OAB$:
:construct $QS$ perpendicular to $OA$
:construct $RS$ perpendicular to $OB$
where $S$ is the point where $QS$ and $RS$ intersect.
Let $OS$ and $PS$ be joined.
Let tangents be constructed at $A$ to the arcs of the great circles $AC$ and $AB$.
These tangents contain the spherical angle $A$.
But by construction, $QS$ and $QP$ are parallel to these tangents.
Hence $\angle PQS = \sphericalangle A$.
Similarly, $\angle PRS = \sphericalangle B$.
Also we have:
{{begin-eqn}}
{{eqn | l = \angle COB
      | r = a
}}
{{eqn | l = \angle COA
      | r = b
}}
{{eqn | l = \angle AOB
      | r = c
}}
{{end-eqn}}
It is to be proved that $PS$ is perpendicular to the plane $AOB$.
By construction, $OQ$ is perpendicular to both $PQ$ and $QS$.
Thus $OQ$ is perpendicular to the plane $PQS$.
Similarly, $OR$ is perpendicular to the plane $PRS$.
Thus $PS$ is perpendicular to both $OQ$ and $OR$.
Thus $PS$ is perpendicular to every line in the plane of $OQ$ and $OR$.
That is, $PS$ is perpendicular to the plane $OAB$.
In particular, $PS$ is perpendicular to $OS$, $SQ$ and $SR$
It follows that $\triangle PQS$ and $\triangle PRS$ are right triangles.
From the right triangles $\triangle OQP$ and $\triangle ORP$, we have:
{{begin-eqn}}
{{eqn | n = 1
      | l = PQ
      | r = OP \sin b
}}
{{eqn | n = 2
      | l = PR
      | r = OP \sin a
}}
{{eqn | n = 3
      | l = OQ
      | r = OP \cos b
}}
{{eqn | n = 4
      | l = OR
      | r = OP \cos a
}}
{{end-eqn}}
Let us denote the angle $\angle SOQ$ by $x$.
Then:
:$\angle ROS = c - x$
We have that:
{{begin-eqn}}
{{eqn | l = OS
      | r = OQ \sec x
}}
{{eqn | l = OS
      | r = OR \, \map \sec {c - x}
}}
{{eqn | ll= \leadsto
      | l = OR \cos x
      | r = OQ \, \map \cos {c - x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = OP \cos a \cos x
      | r = OP \cos b \, \map \cos {c - x}
      | c = from $(3)$ and $(4)$
}}
{{eqn | ll= \leadsto
      | l = \cos a \cos x
      | r = \cos b \paren {\cos c \cos x - \sin c \sin x}
      | c = Cosine of Difference
}}
{{eqn | n = 5
      | ll= \leadsto
      | l = \cos a
      | r = \cos b \cos c + \cos b \sin c \tan x
      | c = dividing both sides by $\cos x$ and multiplying out
}}
{{end-eqn}}
But we also have:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \dfrac {QS} {OQ}
      | c = 
}}
{{eqn | r = \dfrac {PQ \cos A} {OQ}
      | c = 
}}
{{eqn | r = \tan b \cos A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos a
      | r = \cos b \cos c + \cos b \sin c \tan b \cos A
      | c = substituting for $\tan x$ from $(5)$
}}
{{eqn | r = \cos b \cos c + \sin b \sin c \cos A
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}