Finding solution of $\cos x=x$ As mentioned in the post What is the solution of $\cos x=x$, one can obtain the solution by this interesting procedure: start with a 0 on a calculator and keep pressing the cosine button. The sequence of displayed numbers will stabilize pretty quickly and that gives the solution. My question is: why in the first place is this sequence convergent? I can tell from the graph of $y=\cos x$ and $y=x$ but I would like to see an analytical proof.
 A: There's a general theory of function iteration which (among other things) states that if $f$ has a fixpoint $f(x)=x$ with $|f'(x)|<1$, then iterating the function in a neighborhood of the fixpoint will converge towards it.
Since the derivative of the cosine is always less than $1$ except at a few particular points that we can quickly see are not fixpoints, if follows that its fixpoint (which it is also easy to see it must have) must be attractive.
A: Let this sequence be $\{x_n\}_n^\infty$. It is easy to see that $|x_n|\leq 1$. In the following we need the well-known fact that $|\sin x|\leq |x|$. 
Claim: $|x_{n+1}-x_{n+2}|<c|x_n-x_{n+1}|$ for some positive $c<1$.
Proof: \begin{align*}
|\cos x_n-\cos(\cos x_n)|&=\left|2\sin \frac{x_n+\cos x_n}{2}\sin\frac{\cos x_n-x_n}{2}\right|\\
&\leq \left|\sin\frac{x_n+\cos x_n}{2}\right|\cdot|x_n-\cos x_n|\\
&\leq \sin 1\cdot|x_n-\cos x_n|
\end{align*}
Using the claim, we can show that the sequence is Cauchy and hence convergent.
\begin{align*}
|x_n-x_m|&\leq |x_n-x_{n+1}|+\cdots+|x_{m-1}-x_m|\\
&\leq (c^{n-1}+\cdots+c^{m-2})|x_1-x_2|\\
&<\frac{c^{n-1}}{1-c}|x_1-x_2|
\end{align*}
The latter can be made arbitrarily small if $n, m$ are sufficiently large.
