Given the equation $$x^2 + x \cos (x) - 2 \cos ^2 (x) = 0$$ prove it has exactly two real roots.
My attempt
In order two prove the equation indeed just has two real roots, first of all I need to prove they exists and then that they are the only ones.
For the existance part notice that denoting $f(x) = x^2 + x \cos (x) - 2 \cos ^2 (x) = (x-\cos (x))(x+2\cos (x))$ $$f(-2) = 0.0036 > 0, f(0) = -2 < 0, f(1) = 0.00045 > 0$$ By Bolzano's theorem, there is at least one root within each interval $(-2,0)$ and $(0,1)$
Where I am stuck is with the uniqueness part. I tried to find the derivate $$f'(x) = 2x + \cos (x) - x \sin (x) + 4 \cos (x) \sin (x) = 2x + \cos (x) - x \sin (x) + 2\sin (2x)$$ and putting it equal to $0$: $$2x + \cos (x) - x \sin (x) + 2\sin (2x) = 0$$ If I see that this equation only has a root (which is true, checked by graphing it), then by Rolle's theorem a function at most has one root more than it derivative; therefore the two roots I found are the only ones.
However, this is where I got stuck since I can't figure out how to solve this new equation. I think I may be going in the wrong direction, but I can't think of other way to solve the problem. Any help is truly appreciated.
Factorize it
$$(x- \cos x)(x + 2 \cos x) = 0$$
Let
$$g=x-\cos x,~~~~h=x+2\cos x$$
For $g$ part, if $x\in(-\infty, -1]\cup[1,\infty)$, then $g\neq0$. If $x\in(-1,1)$, we have $g'>0$, hence strictly increasing, and easy to check $g(-1)<0<g(1)$. Therefore, $g$ has a unique root on $\mathbb R$.
For $h$ part, if $x\in(-\infty, -2]\cup[2,\infty)$, then $h\neq0$. If $x\in(-2,2)$, we have $h'=1-2\sin x$. Hence $h$ is strictly increasing on $(-2, \frac\pi6)$, and strictly decreasing on $(\frac\pi6, 2)$, and easy to check $h(-2)<0<h(2)<h(\frac\pi6)$. Therefore, $h$ has a unique root on $\mathbb R$.
Last, check the two roots are distinct. Assume they are identical, we get
$$x+2x=0\Longrightarrow x=0$$
and apparently, $g(0)\neq0 \land h(0)\neq 0$, contradiction.