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.

Try this, which I think has some common elements with @egreg’s answer:
Our functions $f$ and $g$ are differentiable, with $f'=g$, $g'=-f$, so that $f^2+g^2=1$ identically, and $|f|\le1$, $|g|\le1$.
For $g$ to have no zero, it must have a limit, $\lim_{x\to\infty}g(x)\ge0$. There are two cases, positive limit or zero; let me treat the latter case first.
If $\>0=\lim_{x\to\infty}g(x)$, then $\lim_{x\to\infty}g'(x)=0$ as well, so $\lim_{x\to\infty}f(x)=0$, contradicting $f^2+g^2=1$.
In case $\lim_{x\to\infty}g(x)=a>0$, then $\forall x, f'(x)\ge a$, and $\forall x\ge0, f(x)\ge ax$ as well, contradicting boundedness of the function $f$.
