In trying to calculate an arc length of a right spherical triangle, I reached this $\arccos$ expression. However, I see the expression given in the manuals for the same problem is much simpler. checking against several values of $\alpha$ and $x$ (Let them both be between $0$ and $\pi/2$) shows those expressions are indeed equivalent.
$$\arctan(\cos(\alpha)*\tan(x)) = \arccos(\dfrac{\cos(x)}{\cos(\arcsin(\sin(\alpha)*\sin(x)))})$$
I tried to prove this equivalence using some trigonometric identities, but I'm quite far it seems.
Best Answer
Notice that $\cos(\arcsin(x)) = \sqrt{1 - x^2}$ by drawing a triangle where $\sin\theta = x$.
Similarly, $\tan(\arccos(x)) = \frac{\sqrt{1 - x^2}}{x} = \sqrt{\frac{1}{x^2} - 1}$.
Now \begin{align*}\tan(RHS) &= \tan\arccos\big(\cos x\cdot\frac{1}{\sqrt{1 - (\sin\alpha\sin x)^2}}\big) \\ &= \sqrt{\frac{1}{\big(\cos x\cdot\frac{1}{\sqrt{1 - (\sin\alpha\sin x)^2}}\big)^2} - 1} \\ &= \sqrt{\frac{1 - \sin^2\alpha\sin^2 x}{\cos^2 x} - 1} \\ &= \sqrt{\frac{\sin^2 x(1 - \sin^2\alpha)}{\cos^2 x}} \\ &= \tan x\cos\alpha\end{align*}
as desired.