Real cosine function/One zero between 0 and 2/Fact/Proof

Proof

We consider the cosine series

${}\cos x=\sum _{n=0}^{\infty }{\frac {(-1)^{n}x^{2n}}{(2n)!}}\,.$

For ${}x=0$, we have ${}\cos 0=1$. For ${}x=2$, one can write

${}{\begin{aligned}\cos 2&=1-{\frac {2^{2}}{2!}}+{\frac {2^{4}}{4!}}-{\frac {2^{6}}{6!}}+{\frac {2^{8}}{8!}}-\ldots \\&=1-{\frac {2^{2}}{2!}}{\left(1-{\frac {4}{3\cdot 4}}\right)}-{\frac {2^{6}}{6!}}{\left(1-{\frac {4}{7\cdot 8}}\right)}-\ldots \\&=1-2(2/3)-\ldots \\&\leq -1/3.\end{aligned}}$

Hence, due to the intermediate value theorem, there exists at least one zero in the given interval.
To prove uniqueness, we consider the derivative of cosine, which is

${}\cos 'x=-\sin x\,,$

due to fact. Hence, it is enough to show that sine is positive in the interval ${}]0,2[$, because then cosine is strictly decreasing by fact in the interval and there is only one zero. Now, for ${}x\in {]0,2]}$, we have

${}{\begin{aligned}\sin x&=x-{\frac {x^{3}}{3!}}+{\frac {x^{5}}{5!}}-{\frac {x^{7}}{7!}}+\ldots \\&=x{\left(1-{\frac {x^{2}}{3!}}\right)}+{\frac {x^{5}}{5!}}{\left(1-{\frac {x^{2}}{6\cdot 7}}\right)}+\ldots \\&\geq x{\left(1-{\frac {4}{3!}}\right)}+{\frac {x^{5}}{5!}}{\left(1-{\frac {4}{6\cdot 7}}\right)}+\ldots \\&\geq x/3\\&>0.\end{aligned}}$

To fact