Proof of The Cosine Is Positive on $(-\pi/2,\pi/2)$

Routine arithmetic is used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity). Let $\sin:\mathbb{R}\to\mathbb{R}$ be the sine function, and fix $x\in(-\pi/2,\pi/2)$. The idea is to move $x$ by a quarter period, which turns the cosine into the sine, and then to use that the sine is positive on the half period $(0,\pi)$.

Shift by a quarter period. The quarter-turn identity of Quarter-Turn Identities and Periodicity of Sine and Cosine (iii), applied at the point $x$, gives

$$\cos x=\sin\Bigl(x+\frac{\pi}{2}\Bigr).$$

Positivity of the sine. Adding $\pi/2$ to the inequalities $-\pi/2<x<\pi/2$ gives

$$0<x+\frac{\pi}{2}<\pi ,$$

so the point $x+\pi/2$ lies in the half period on which the sine is positive, and $\sin(x+\pi/2)>0$ by Quarter-Turn Identities and Periodicity of Sine and Cosine (vii). Together with the previous identity this gives $\cos x>0$. As $x\in(-\pi/2,\pi/2)$ was arbitrary, this proves (i).