how to prove this trig inequality: $\cos x \cos y + z \sin x \sin y \geq \cos \left( \sqrt{x^2 + y^2 - 2 x y z} \right)$ The following inequality has come up in my work. I'm trying to prove that it is true:
$$
\begin{equation}
\cos x \cos y + z \sin x \sin y \geq \cos \left( \sqrt{x^2 + y^2 - 2 x y z} \right)
\end{equation}
$$
where
$$
\begin{align}
-\pi \leq{} &x \leq \pi \\
-\pi \leq{} &y \leq \pi \\
-1 \leq{} &z \leq 1
\end{align}
$$
The LHS of the inequality is derived from the spherical law of cosines, the RHS is derived from the law of cosines, and $z$ represents the cosine of another variable. Note that the inequality holds with equality when $z=1$.
I have also put the inequality in the following form using the product-to-sum trig identity, and rearranging the RHS:
$$
\begin{equation}
(1+z) \cos(x-y) + (1-z) \cos(x+y) \geq 
2 \cos \left( \sqrt{(x-y)^2 + 2 x y (1-z)} \right)
\end{equation}
$$
I have also tried other things like applying Cauchy-Schwarz to the LHS, and applying arccosine to both sides, but I can't seem to prove that the inequality is true.
I am quite certain that the inequality holds because I have performed a Monte Carlo simulation (code shown below) which shows that the inequality holds for randomly sampled values.

python Monte Carlo random sampling code
import numpy as np

n = 10**6
x = np.random.uniform(-np.pi, np.pi, n)
y = np.random.uniform(-np.pi, np.pi, n)
z = np.random.uniform(-1, 1, n)
lhs = np.cos(x)*np.cos(y) + z*np.sin(x)*np.sin(y)
rhs = np.cos(np.sqrt(x**2 + y**2 - 2*x*y*z))
check = lhs>=rhs
print('inequality is true', np.sum(check), '/', n, 'times')

 A: Replacing $(x, z)$ by $(-x, -z)$ or $(y, z)$ by $(-y, -z)$ does not change the inequality, therefore we can assume that
$$
 0 \le x, y \le \pi  \, , \, -1 \le z \le 1 \, .
$$
Case 1: $x+y \le \pi$. The solution for this case is inspired by Proving that $\cosh^{-1} (\cosh(x)\cosh(y) ) \geq \sqrt{x^2 + y^2}$ and the CAT(0) inequality.
The function $f(u) = \cos(\sqrt u)$ is convex on the interval $0 \le u \le \pi^2$, this is straightforward to verify, e.g. by calculating the second derivative.
We can assume that $y \le x$. The convexity condition with $\lambda = (1+z)/2$ and $1-\lambda = (1-z)/2$ then gives
$$
\begin{align}
\cos x \cos y + z \sin x \sin y &= 
\frac{1+z}2 \cos(x-y) + \frac{1-z}2 \cos(x+y) \\
 &= \frac{1+z}2 f((x-y)^2) + \frac{1-z}2 f((x+y)^2) \\
&\ge f \left( \frac{1+z}2 (x-y)^2 + \frac{1-z}2 (x+y)^2\right) \\
&= f( x^2+y^2-2xyz) \\
&= \cos \left( \sqrt{x^2 + y^2 - 2 x y z} \right) \, .
\end{align}
$$
$f$ is in fact strictly convex, so that equality holds exactly in the following cases:

*

*$\lambda = 0$ or $1$, that is if $z = \pm 1$.

*$(x-y)^2 = (x+y)^2$, that is if $x=0$ or $y=0$.

Case 2: $\pi < x+y \le 2\pi$. This case can be reduced to the first case, credit goes to ipst. I have only simplified the solution a bit.
Setting $x' = \pi - x$ and $y' = \pi - y$ we can apply the first case to $(x', y', z)$:
$$
\begin{align}
 \cos x \cos y + z \sin x \sin y &= \cos x' \cos y' + z \sin x' \sin y' \\
 &\ge \cos \left( \sqrt{x'^2 + y'^2 - 2 x' y' z} \right) \\
 &\overset{(*)}{\ge} \cos \left( \sqrt{x^2 + y^2 - 2 x y z} \right) \, .
\end{align}
$$
The last inequality $(*)$ needs to be proved. For $\alpha, \beta \in [0, 2 \pi]$ we have
$$
 \cos \alpha  \ge \cos \beta \iff \alpha \le \beta \le 2\pi -\alpha \, .
$$
Therefore we have to show that
$$
\sqrt{x'^2 + y'^2 - 2 x' y' z} \overset{(1)}{\le} \sqrt{x^2 + y^2 - 2 x y z}\overset{(2)}{\le} 2 \pi - \sqrt{x'^2 + y'^2 - 2 x' y' z} \, .
$$
The left part $(1)$ follows from
$$
(x^2 + y^2 - 2 x y z) - (x'^2 + y'^2 - 2 x' y' z) = 2 \pi(x+y-\pi)(1-z) \ge 0
$$
and the right part $(2)$ follows from
$$
\sqrt{x^2+y^2-2xyz} + \sqrt{x'^2+y'^2-2x'y'z}
\le (x+y) + (x'+y') = 2 \pi \, .
$$
Equality holds in the following cases:

*

*$z = \pm 1$.

*$x'y' = 0$ and $x+y= \pi$, that is if $(x, y) = (\pi, 0)$ or $(x, y) = (0, \pi)$.

A: I think if $0\le y\le x\le \pi$ and $x+y>\pi$, you can take $x'=\pi-x$ and $y'=\pi-y$ and use Martin R's proof with $x',y',z$ instead.  It works because $x'+y'=2\pi-x-y<\pi$ and $$(x'^2+y'^2-2x'y'z)-(x^2+y^2-2xyz)=-2\pi(1-z)(x+y-\pi)\le 0$$ so $$\cos\sqrt{x'^2+y'^2-2x'y'z}\ge \cos\sqrt{x^2+y^2-2xyz}$$
while
$$\cos x'\cos y'+z\sin x' \sin y'=\cos x\cos y+z\sin x\sin y.$$
Apparently there is another equality condition $x,y=\pm \pi$ and $z=\pm 1$.
From Martin R comment below, I need
$$\sqrt{x'^2+y'^2-2x'y'z}\le \sqrt{x^2+y^2-2xyz}\le 2\pi -\sqrt{x'^2+y'^2-2x'y'z}.$$
I proved only the inequality on the left.  Not yet on the right.  After trying to prove the right inequality, I got this messy inequality to prove
$$(1+z)\Big[(x+y+\pi)^2-4(x^2+y^2)+z(x+y-\pi)^2\Big]\ge 0.$$
This is true because $1+z\ge 0$ and
$$(x+y+\pi)^2-4(x^2+y^2)+z(x+y-\pi)^2\ge (x+y+\pi)^2-4(x^2+y^2)-(x+y-\pi)^2 = 4x(\pi-x)+4y(\pi-y)\ge 0.$$
