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$
From the right triangles $\triangle OSQ$ and $\triangle OSR$, we have:
{{begin-eqn}}
{{eqn | l = QS
      | r = OS \sin x
}}
{{eqn | l = RS
      | r = OS \, \map \sin {c - x}
}}
{{eqn | ll= \leadsto
      | l = RS \sin x
      | r = QS \paren {\sin c \cos x - \cos c \sin x}
      | c = Sine of Difference
}}
{{eqn | ll= \leadsto
      | l = RS
      | r = QS \paren {\sin c \cot x - \cos c}
      | c = dividing both sides by $\sin x$
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = RS
      | r = PR \cos B
}}
{{eqn | r = OP \sin a \cos B
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = QS
      | r = PQ \cos A
}}
{{eqn | r = OP \sin b \cos A
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = QS \cot x
      | r = OQ
}}
{{eqn | r = OP \cos b
}}
{{end-eqn}}
from which it follows that:
:$\sin a \cos B = \cos b \sin c - \sin b \cos c \cos A$
The result follows.