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.
 A: To the first question : if sine starts from zero and increases, it is positive.
So the derivative of cosine $g'=-f $ is negative.
Hence cosine decreases.
Added
To the second question: as cosine starts from $1$ at $x=0$ and decreases, it either reaches zero at some $x_0 > 0$, or not.
So there exists $a$ such that $1 = \cos 0 > \cos a > 0$  (that would be any $a>0$ in the latter case, or some $0<a<x_0$ in the former).
Then, the positive value less than $1$, when raised to a positive power $2^n$, results in decreasing values as $n$ grows (we get a fraction of the same fraction of the fraction, and so on).
However, it never gets negative, as a product of two positive values $(\cos a)^{2^n}\,\cdot\,(\cos a)^2$ makes a positive result.
As a result we get a strictly decreasing positive sequence of cosine's values at $x_n=2^na$.
But we know the function is strictly decreasing, so its values between $x_n<x_{n+1}$ are between $\cos(x_n)$ and $\cos(x_{n+1})$, hence positive, too, and bounded from above by decreasing  $\cos(x_n) = (\cos a)^{2^n}$ as $n$ grows.
This 'squeezes' the cosine towards zero.
I wonder. however, how did author get the identity $$g(2a)=(g(a))^2−(f(a))^2$$ just form the presented assumptions...
A: The conditions immediately imply that the derivative of $f(x)^2+g(x)^2$ is $0$. So $f(x)^2+g(x)^2=f(0)^2+g(0)^2=1$ for all $x$.
If $f'(x)>0$ for all $x\ge 0$ then  $\forall t>1\,(-f(t)<-f(1)<-f(0)=0)$. But then $$x>1\implies g(x)-g(1)=\int_1^xg'(t)dt=\int_1^x(-f(t))dt<$$ $$<\int_1^x(-f(1))dt=(x-1)(-f(1))\implies$$ $$\implies \lim_{x\to\infty}g(x)=-\infty$$ contrary to $ g(x)^2=1-f(x)^2\le 1.$
So there must exist $x_1>0$ with $f'(x_1)\le 0.$ And since $f'=g$ is continuous with $f'(0)>0$ there must exist $x_2\in (0,x_1]$ with $0=f'(x_2)=g(x_2).$
A: If $\cos x>0$ for every $x$, then the sine is strictly increasing. But in the definition it is assumed that $\sin 0=0$. Hence $\sin x>0$ for $x>0$.
And now, the fact that $\cos'x=-\sin x$ tells us that the cosine is strictly decreasing over $(0,\infty)$.
Now you know that $0<\cos x<1$ for every $x>0$: indeed, $\cos x=1$ implies $\sin x=0$, but we have proved that $\sin x>0$ when $x>0$. A bounded and decreasing function has a limit at $\infty$, precisely the infimum of its range (this is known for every such function defined over an upper unbounded interval) and in order to find the limit it's sufficient to find the limit over a sequence that has infinite limit. The chosen sequence is $(2^na)$ and it shows that
$$
\lim_{x\to\infty}\cos x=0
$$
Hence
$$
\lim_{x\to\infty}\sin x=1
$$
using $\sin^2x=1-\cos^2x$ and the fact that the sine is increasing.
A: 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$.
A: $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.
