Geometrically, I have strong reasons to believe that the following inequality holds:
$\arccos\left(\cos\alpha \cos\beta - \sin\alpha \sin\beta \cos\varphi\right) \leq \sqrt{\alpha^2 + \beta^2 - 2 \alpha \beta\cos\left(\pi-\varphi\right)}$
Analytically, my first approach was to determine the stationary points of the function
$\operatorname{f}\left(\alpha, \beta, \varphi\right) = \arccos\left(\cos\alpha \cos\beta - \sin\alpha \sin\beta \cos\varphi\right) - \sqrt{\alpha^2 + \beta^2 - 2 \alpha \beta\cos\left(\pi-\varphi\right)}$
Unfortunately, I wasn't able to solve $\nabla \operatorname{f} = 0$ for $\alpha, \beta$ and $\varphi$ analytically. Would it be a good idea to look for zero crossings of $\nabla \operatorname{f}$ numerically and afterwards proof their exact solution? How could I then proof that I didn't miss an intermediate extremum?
Are there any ways to simplify the equation further? Am I taking the correct approach here at all?