Convergent subsequence for sin(n)

Define a sequence $(a_n)_{n = 1}^{\infty}$ of real numbers by $a_n = \sin(n)$. This sequence is bounded (by $\pm1$), and so by the Bolzano-Weierstrass Theorem, there exists a convergent subsequence.

My question is this: Is there any way to construct an explicit convergent subsequence?

Naïvely, I tried considering the subsequence $$\sin(3), \,\sin(31), \,\sin(314), \,\sin(3141),\, \sin(31415),\, \dots$$ hoping it would converge to $0$, but I was unable to prove this (and I think it's probably not even true).

• You can come up with a subsequence that converges to $1$ (or any other value you choose in $[-1,1]$): Let $a_1=\sin(1)$. Then let $a_2=\sin(k_2)$ where $k_2$ is the least integer for which $\sin(k_2)\geq \sin(1)$. In general, let $a_n = \sin(k_n)$ where $k_n$ is the least integer for which $\sin(k_n) \geq \sin(k_{n-1})$. A similar process gives a subsequence that converges to any value in $[-1,1]$ you choose. The proof shouldn't be too taxing. However, it would be quite a push to call this an explicit subsequence. May 21 '14 at 7:27

This isn't a very analytic way of doing it but consider the continued fraction expansion $\pi = [a_0; a_1, a_2, \ldots]$. Generally we know that, if $p_n/q_n$ are the convergents to $\pi$ then $|q_n\pi - p_n| \leq 1/q$ so the $p_n$ are the closest integers to being multiples of $\pi$ so (with slight abuse of notation) $\sin(p_n) \rightarrow \sin m\pi = 0$ with $n \rightarrow \infty$ meaning that this is an explicit construction of the sort that you're after.
• I've just realised that I've written this in a really weird way, you want are the numerators of the convergents $p_n$ so the sequence starts $3, 22, 333, 355, 103993, \ldots$ and then $\sin$ of this sequence tends to $0$ pretty darn quickly. May 21 '14 at 7:47
I am not very confident that it converges, because this is how well you can approximate $10^k \cdot \pi$ with an integer. But as the difference will be infinite many times greater than $0.9$ and as you get bounds you see that this sequence is divergent.
I think this is more a question what is explicit for you, because you need to know how well you can approximate a multiple of $\pi$ with an Integer.