The Least Positive Zero of the Cosine

In the setting of The Real Numbers: Standing Notation and Background, let $\cos$ and $\sin$ be the cosine and sine functions from $\mathbb{R}$ to $\mathbb{R}$, and let $3=1+1+1$. Then the following hold.

1. (The least positive zero)(i) There is exactly one real number $x_{0}$ such that

$$0<x_{0}, \qquad \cos x_{0}=0, \qquad\text{and}\qquad 0<\cos t\ \text{ for every real }t\text{ with }0\le t<x_{0}.$$

It satisfies $x_{0}\le3$.

2. (The sine up to that point)(ii) With $x_{0}$ as in clause 1, one has $0<\sin t$ for every real $t$ with $0<t\le x_{0}$, and $\sin x_{0}=1$.