Does the proof of Bolzano-Weierstrass theorem require axiom of choice?

When selecting the terms of subsequence from each bisections, I thought axiom of choice might be required. But I'm not so sure whether or not, so please tell me.
[edited]
I'm sorry for the lack of explanation. I want to prove this statement:
Let $a_1, a_2, \ldots \in \mathbf{R}$, and $(a_n)_{n\in\mathbf{N}}$ is bounded, then $(a_n)$ has some convergent subsequence.

The proof is as follows. Since $(a_n)$ is bounded, for all $n\in\mathbf{N}$, $a_n \in I = [b, c]$.
Now, let $I_0 = I$ and if $I_n = [b_n, c_n]$, we define $d_n = (b_n+c_n)/2$ and if infinite terms of $(a_n)$ is included in $[b_n, d_n]$(resp. $[d_n, c_n]$), we will define $I_{n+1} = [b_n, d_n]$(resp. $[d_n, c_n]$).If both intervals contain infinite terms, let $I_{n+1}$ be $[d_n, c_n]$.
For all $n\in \mathbf{N}$, infinite numbers of $m \in \mathbf{N}$ exist such that $a_m \in I_n$ suffices. We take the sequence of natural numbers $(n(k))_{k\in\mathbf{N}}$which suffices $n(0) < n(1) < \cdots < n(k) < \cdots$ following this procedure:
Now we have already selected $a_{n(1)}, \ldots, a_{n(k)}$, there are infinite numbers of $m\in \mathbf{N}$ which suffices $n(k)<m, a_m \in I_{k+1}$, so let's take the minimum m out of it. Applying this process recursively, we obtain a infinite convergent subsequence(?).
I think intuitively, by only repeating this process we can't obtain countable infinite terms of subsequence because we have to repeat infinite times.

Solution 1:

I would like to explain why the proof above do not need to use the axiom of choice. When you said ''so let's take the minimum m out of it'' you have done a defined choice. If someone else do you proof he will ''choose'' the same ''m'' as you because the way the choice is done is specified. This choice is done infinitely many times. However, assume that (which is not true) there is no minimum m among the integers greater than n(k), or assume that (which is not true too) that the minimum exists but is not unique, so you have no way to point your finger to it you have no way to define it precisely, you will only say, ''ok, since i know there are infinitely many such convenient m then i choose one of them, any one of them is ok!'' this way you take m needs the axiom of choice! I invite you to read the example given by Bertrand RUSSEL concerning the way to choose shoes and sockets; assume there are infinitely many pairs of shoes and you want to choose one from each pair then you can specify your choice from each pair by saying for example, the left one from each pair, or the right one from each, this choice is possible because you can distinguish at least one shoe from the pair of shoes, for each pair of shoes. But what about if the pairs are indistinguishable as sockets pairs. This time you need the axiom of choice. In your proof, the set of convenient m contains a distinguished element which is the minimum one and it is this you choose. so no need to the axiom of choice.

Solution 2:

There's no issue with the axiom of choice here.

We construct increasingly longer initial segments of our subsequences. This is like looking at some tree of finite sequences of natural numbers. The tree itself is already provably well-orderable. So the existence of a branch, the infinite sequence, is not using the axiom of choice.