Triangular inequality of spherical distance

Question

If $a=(a_1,a_2,a_3)$ and $b=(b_1,b_2,b_3)$ are points on a unit sphere, the distance from $a$ to $b$ along the surface of the sphere is $d(a,b)=\arccos(a\cdot{} b)=\arccos(a_1b_1+a_2b_2+a_3b_3)$. But does this distance function satisfy the triangle inequality?

Answer 1

In a word "yes." Geometrically, this function is the great circle distance. This is the infimum of arc lengths of piecewise-smooth paths, which "obviously" satisfies the triangle inequality because a concatenation of two piecewise-smooth paths is piecewise-smooth.

There are also proofs based on judicious choices of coordinates, and/or spherical trigonometry, but I don't have references offhand.