One of my books gives the following proof that if the image of a sequence of real numbers $x_n$ has an accumulation point $x_0$, then there exists a subsequence $x_{n_k}$ convergent to $x_0$.
The sequence having finitely many values is a trivial case, so let's consider the case where there are infinitely many points in it.
We consider the intersections between the sequence and the balls of radius $\frac{1}{k}$, $k \in \mathbb{N}$, centered in $x_0:$ $$U_k =B_{\frac{1}{k}}(x_0) \ \cap \ \{x_n\}_{n \in \mathbb{N}}$$
Since $x_0$ is an accumulation point, $U_k$ contains infinitely many points of the sequence, for every $k$.
We define a subsequence as follows:
- we choose any point in $U_1$ as our first point, call its index $n_1$;
- since there are infinitely many points in $U_2$, infinitely many of them have an index greater than $n_1$. Choose one and call its index $n_2$;
- ...
- since there are infinitely many points in $U_{k+1}$, infinitely many of them have an index greater than $n_k$. Choose one and call its index $n_{k+1}$;
- and so on.
The subsequence $x_{n_k}$ converges to $x_0$.
Is the Axiom of Choice needed to justify this definition procedure? I'm used to books always pointing out when they use AC, but in this case my book doesn't.
The book also doesn't mention it, but by the well-ordering of the naturals, the iterative process can be made more "canonical" and less "choosy" by always defining $n_{k+1}$ as the minimal element of the set $\{n \ | \ n>n_k \land x_n \in U_{k+1} \}$.
Would this make AC unneeded? Was it unneeded in the first place, even with the book's procedure?