Looking at the proof of Bolzano–Weierstrass theorem, it found an interesting lemma (called the peak lemma here) :
Every sequence $(x_n)_{n\in \mathbb{N}}\in \mathbb{R}^\mathbb{N}$ has a monotone subsequence.
Looking at the French Wikipedia article about subsequence, it says that the proof of the peak lemma doesn't give an explicit construction of the monotone subsequence. In particular, for the sequence $(\sin(n))_{n\in \mathbb{N}}$, we don't know a closed-form expression for a subsequence $(n_k)_{k\in \mathbb{N}}$ such that $(\sin(n_k))_{k\in \mathbb{N}}$ is monotone. But there is no reference for this fact. So my question is: do you have any references in this direction?
An additional question is also: do we have a simple (meaning it uses basic functions and/or satisfies a simple recurrence relation) example of a sequence for which we know an explicit (and nontrivial...), ie with a closed-form expression for the subsequence indexes, construction of a monotone subsequence?