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)¶ There is exactly one real number $x_{0}$ such that

It satisfies $x_{0}\le3$.

2. (The sine up to that point)¶ 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$.