Show that the angle function between two points on the unit circle satisfies the triangle inequality With $S^1$ as the unit circle:
$$
  S^1 = \{ x \in \mathbb{R}^2 \mid x_1^2 + x_2^2 = 1 \} \\
$$
And with $\arg$ as the well defined argument function that returns the principle value:
$$
  \arg(x) : \mathbb{C} \to (-\pi,+\pi]
$$
We can define the angle distance function as:
\begin{align*}
  \angle &: S^1 \times S^1 \to [0,\pi] \\
  \angle(x,y) &= | \arg((x_1 + i \cdot x_2) / (y_1 + i \cdot y_2)) | \\
\end{align*}
What we want to show is:
\begin{align*}
  \angle(x,z) &\le \angle(x,y) + \angle(y,z) \\
  | \arg((x_1 + i \cdot x_2) / (z_1 + i \cdot z_2)) | &\le | \arg((x_1 + i \cdot x_2) / (y_1 + i \cdot y_2)) | + | \arg((y_1 + i \cdot y_2) / (z_1 + i \cdot z_2)) | \\
\end{align*}
I'm stuck on what to do next
 A: The main idea is that $\arg(z_1/z_2)=\arg(z_1)-\arg(z_2)$. Hence, for three complex numbers, $x,y,z$, we can say
$$
|\arg(z)-\arg(x)|=|\arg(z)-\arg(x)+\arg(y)-\arg(y)|.
$$
A: It is easy to give a geometric proof - let $x=A, y=B, z=C$ points on the unit circle; then $\angle(x,y) = \widehat {AB}$, the length of the minor arc joining them on the circle ( obviously $\angle(x,y)=\pi$ iff $AB$ diameter). But then if $C$ is on the minor arc $\widehat {AB}$ we have equality $\widehat {AB}=\widehat {AC}+\widehat {CB}$, otherwise either $A$ is on the minor arc $\widehat {CB}$ or $B$ is on the minor arc $\widehat {AC}$, or the minor arcs $\widehat {AB}, \widehat {BC},\widehat {CA}$ span the circle and in all case the inequality is obvious as in the first two cases $\widehat {AB} \le \widehat {AC}$ or $\widehat {BC}$ as in the second $\widehat {AB} \le \pi \le \widehat {BC} +\widehat {CA}$
A: To complete this problem with help from zugzug and the others:
We can define the angle distance function as follows with $k$ as the appropriate integer constant to result in a value in $[0,\pi]$:
\begin{align*}
  \angle &: S^1 \times S^1 \to [0,\pi] \\
  %\angle(x,y) &= \abs{\arg((x_1 + i \cdot x_2) / (y_1 + i \cdot y_2))} \\
  \angle(x,y) &= \arg(x_1 + i \cdot x_2) - \arg(y_1 + i \cdot y_2) + 2k\pi \\
\end{align*}
\begin{align*}
  \angle(x,z) &= \arg(x_1 + i \cdot x_2) - \arg(z_1 + i \cdot z_2) + 2k\pi \\
  \angle(x,y) &= \arg(x_1 + i \cdot x_2) - \arg(y_1 + i \cdot y_2) + 2k\pi \\  
  \angle(y,z) &= \arg(y_1 + i \cdot y_2) - \arg(z_1 + i \cdot z_2) + 2k\pi \\  
\end{align*}
With some algebra:
\begin{align*}
  \angle(x,z) &= \angle(x,y) + \angle(y,z) + 2k'\pi \\
\end{align*}
In this last expression, $k'$ can be either $0$ or $-1$ so we can conclude that:
\begin{align*}
  \angle(x,z) &\le \angle(x,y) + \angle(y,z) \\
\end{align*}
