Lang's proof that there exists $x>0$ such that $\cos x=0$ In Undergraduate Analysis on p. 90, Lang assumes the existence of two functions $f$ (sine) and $g$ (cosine) satisfying the conditions $f(0)=0$, $g(0)=1$, $f'=g$ and $g'=-f$. He then goes on to show that there exists $x>0$ such that $\cos x=0$.
With your help, I would like to make some of the steps in his proof more explicit.

Suppose that no such number exists. Since $\cos$ is continuous, we
conclude that $\cos x$ cannot be negative for any value $x>0$ (by
intermediate value theorem). Hence $\sin$ is strictly increasing for
all $x>0$, and $\cos x$ is strictly decreasing for all $x>0$...

It's clear why $\sin$ is strictly increasing on the interval $(0,\infty)$. Why is $\cos$ strictly decreasing on the interval $(0,\infty)$? This would require $\sin x>0$ for all $x\in(0,\infty)$. But how can I show this?

... Let $a>0$. Then $0<\cos 2a=\cos^2a-\sin^2a<\cos^2a$. By induction,
we see that $\cos(2^n a)<(\cos a)^{2^n}$ for all positive integers
$n$. Hence $\cos(2^na)$ approaches $0$ as $n$ becomes large, because
$0<\cos a<1$. Since $\cos$ is strictly decreasing for $x>0$, it
follows that $\cos x$ approaches $0$ as $x$ becomes large, and hence
$\sin x$ approaches $1$. In particular, there exists a number $b>0$
such that $$\cos b<\frac{1}{4}\text{ and }\sin b>\frac{1}{2}.$$

If $\lim_{n\rightarrow\infty}\cos(2^na)=0$ for all $a>0$, how can I conclude that $\lim_{x\rightarrow\infty}\cos x=0$? Let $\epsilon>0$. Then I would have to show that there exists $s\in\mathbb{R}$ such that
$$(\forall x)(x\in(s,\infty)\implies|\cos x|<\epsilon).$$
It's not immediately clear how to find such an $s$. I would have to use the fact that $\lim_{n\rightarrow\infty}\cos(2^na)=0$ for all $a>0$, but I don't know how.

$n \in \mathbb{Z} \rightarrow +\infty$ can be interpreted as $n \in \mathbb{N} \rightarrow +\infty$.
In other words, as $n$ approaches positive infinity, we can ignore the negative values.
$\forall x \in \mathbb{N} \ \exists \ r \in \mathbb{R} \ \mid \ 2^r = x$
(as $f$ strictly increasing and the statement that is true for integers, it is true for reals, except when $f$ is undefined for a specific number)
$a \ 2^n = 2^{m} \ \mid \ m \in \mathbb{R}$
Therefore $x$ can be written as $a \ 2^n$, then as $s$ gets bigger, the threshold becomes smaller.
