Initial program 24.5
\[R \cdot \left(2 \cdot \tan^{-1}_* \frac{\sqrt{{\left(\sin \left(\frac{\phi_1 - \phi_2}{2}\right)\right)}^{2} + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}{\sqrt{1 - \left({\left(\sin \left(\frac{\phi_1 - \phi_2}{2}\right)\right)}^{2} + \left(\left(\cos \phi_1 \cdot \cos \phi_2\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right)}}\right)\]
Initial simplification24.5
\[\leadsto \tan^{-1}_* \frac{\sqrt{\left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) + \sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(R \cdot 2\right)\]
- Using strategy
rm Applied add-log-exp24.5
\[\leadsto \tan^{-1}_* \frac{\sqrt{\left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) + \sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \color{blue}{\log \left(e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}\right)}\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(R \cdot 2\right)\]
- Using strategy
rm Applied add-sqr-sqrt24.5
\[\leadsto \tan^{-1}_* \frac{\sqrt{\left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) + \sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \log \color{blue}{\left(\sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}} \cdot \sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}\right)}\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(R \cdot 2\right)\]
Applied log-prod24.5
\[\leadsto \tan^{-1}_* \frac{\sqrt{\left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) + \sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \color{blue}{\left(\log \left(\sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}\right) + \log \left(\sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}\right)\right)}\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(R \cdot 2\right)\]
- Using strategy
rm Applied div-sub24.5
\[\leadsto \tan^{-1}_* \frac{\sqrt{\left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) + \sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \left(\log \left(\sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}\right) + \log \left(\sqrt{e^{\sin \color{blue}{\left(\frac{\lambda_1}{2} - \frac{\lambda_2}{2}\right)}}}\right)\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(R \cdot 2\right)\]
Applied sin-diff24.6
\[\leadsto \tan^{-1}_* \frac{\sqrt{\left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) + \sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \left(\log \left(\sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}\right) + \log \left(\sqrt{e^{\color{blue}{\sin \left(\frac{\lambda_1}{2}\right) \cdot \cos \left(\frac{\lambda_2}{2}\right) - \cos \left(\frac{\lambda_1}{2}\right) \cdot \sin \left(\frac{\lambda_2}{2}\right)}}}\right)\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(R \cdot 2\right)\]
Final simplification24.6
\[\leadsto \tan^{-1}_* \frac{\sqrt{\sin \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \sin \left(\frac{\phi_1 - \phi_2}{2}\right) + \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right) \cdot \left(\cos \phi_2 \cdot \sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)\right)}}{\sqrt{\cos \left(\frac{\phi_1 - \phi_2}{2}\right) \cdot \cos \left(\frac{\phi_1 - \phi_2}{2}\right) - \left(\cos \phi_2 \cdot \left(\log \left(\sqrt{e^{\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right)}}\right) + \log \left(\sqrt{e^{\cos \left(\frac{\lambda_2}{2}\right) \cdot \sin \left(\frac{\lambda_1}{2}\right) - \sin \left(\frac{\lambda_2}{2}\right) \cdot \cos \left(\frac{\lambda_1}{2}\right)}}\right)\right)\right) \cdot \left(\sin \left(\frac{\lambda_1 - \lambda_2}{2}\right) \cdot \cos \phi_1\right)}} \cdot \left(2 \cdot R\right)\]