By Wikipedia article on Axiom of dependent choice, it is necessary to have it for development of real analysis. The ${\mathsf {DC}}$ says:
Axiom (${\mathsf{DC}}$). For any nonempty set $X$ and every entire binary relation $\sim$ on $X$ there is a sequence $(x_n)_{n\in\mathbb{N}}$ s.t. $x_n\sim x_{n+1}$ for all $n\in\mathbb{N}$.
I was looking for some examples of theorems in real analysis for which this axiom is necessary. Could this be an example?
Theorem: Number $\alpha\in\overline{\mathbb{R}}$ is a limit point of sequence $(a_n)_{n\in\mathbb{N}}$ if and only if there exists a sub-sequence $(a_{k_n})_{n\in\mathbb{N}}$ such that $a_{k_n}\rightarrow \alpha$.
Proof. $\Leftarrow:$ In every neighbourhood of $H_\alpha$ lies infinitely many members of $(a_{k_n})$ thus infinitely many of $(a_n)$.
$\Rightarrow:$Assume neighbourhood $H_\alpha(1)$. $\alpha$ is a limit point, so there exists some $k_1$ s.t. $a_{k_1}\in H_\alpha(1)$. If $n\in\mathbb{N},n>1$, for neighbourhood $H_\alpha(1/n)$ there exists $k_n>k_{n-1}$ satisfying $a_{k_n}\in H_\alpha(1/n)$. Such constructed sequence converges to $\alpha$.
Now, this seems that we actually used the dependent choice in each step to construct the entire sequence. Without $\mathsf{DC}$, we could only construct a finite one, am i correct?
Another example:
Theorem (Bolzano-Weierstrass): Every bounded sequence has a limit point $\alpha\in\mathbb{R}$.
Proof. Let $(a_n)_{n\in\mathbb{N}}$ be bounded. Thus $\{a_n\}\subseteq [b_1,c_1]$ where $[b_1,c_1]$ denotes real interval. Now we split this interval into two: $$\left[b_1,\frac{b_1+c_1}{2}\right],\left[\frac{b_1+c_1}{2},c_1\right]$$ Atleast one of these contains infinitely many terms of $(a_n)$. Denote it by $[b_2,c_2]$. Following these steps, we construct a sequence of intervals $([b_n,c_n])$. For which $[b_k,c_k]\subseteq[b_{k-1},c_{k-1}]$ for all $k\in\mathbb{N}$ and also their lengths converge to $0$. By nested intervals theorem (or axiom) there is a real number $x$ contained in each of $[b_n,c_n]$. By assumption, $[b_n,c_n]\rightarrow 0$ thus for any $\epsilon>0$ there is $n_0$ s.t. $[b_{n_0},c_{n_0}]<\epsilon$. So for any neighbourhood $H_x$ there is such $n_{0}$ large enough such that $[b_{n_0},c_{n_0}]\subseteq H_x$. But each of $[b_{n},c_{n}]$ for $n>n_0$ contains still infinitely many terms of $(a_n)$ thus $x$ is a limit point of $(a_n)$.
Again, we did use the dependent choice, didn't we? In each step, we are forced to add a new interval, because after split, in atleast one of them there must be infinitely many terms of $(a_n)$. Does the dependent choice here allow us to construct the entire sequence like this? Without it, we would be only able to construct a finite one
Let's give last example from ordering.
Theorem: Let $(S,<_S)$ be a poset. Then $(S,<_S)$ is well-ordered if and only if there is no infinite sequence $(a_n)$ in $S$ s.t. $\forall n \in\mathbb{N}: a_{n+1}<_Sa_n$
Proof $\Leftarrow :$ (contrapositive). Assume $<_S$ is not well ordering. Thus there is a set $T\subseteq S$ s.t. $T$ has no least element. Let $a_1\in T$ be arbitrary. Because $a_1$ has no least element, there is some $x\in T$ s.t. $x<_Sa_1$. Set $a_2=x$. Do the same process to construct monotone sequence $(a_n)$.
$\Rightarrow$ (contrapositive). Assume an infinite monotone sequence $(a_n)$ in $S$ exists. Set $T=\{a_n\mid n\in\mathbb{N}\}$ (the elements of sequence $(a_n)$). $T$ obviously has no least element, thus $<_S$ is not well ordered.
Again, (in the $\Leftarrow$ part) we were forced to have some $x$ below $a_1$. Without $\mathsf{DC}$ we wouldn't be able to construct the entire sequence. Is that correct?
I am not looking for correctness of the proofs given above, they are correct . I am just looking for justification of my thoughts on this deeper leverl and if they're correct. On the other hand, let's make a big list of rather "trivial" statements which may seem to hide $\mathsf{AC}$ or some of its weaker forms.
Typically, even DC is unnecessary for basic results in real analysis. It can usually be avoided by using the fact that "reals are countably approximable," in one of the two following forms:
The topology for $\mathbb{R}$ is second countable - it has as a base the set of all open intervals with rational endpoints.
The topology for $\mathbb{R}$ is separable - $\mathbb{Q}$ is a countable dense set.
(Actually, what we're really using is well-orderable approximability - countability isn't relevant here, the point is that countable sets are well-orderable - but talking about countable approximability is probably more concrete at first.)
For example, here's how we can use the first point to give a choice-free proof of Bolzano-Weierstrass. Let $(I_i)_{i\in\mathbb{N}}$ enumerate the rational open intervals, and let $A=(a_j)_{j\in\mathbb{N}}$ be our sequence. For each $n\in\mathbb{N}$, let $k_n$ be the least natural number such that
$I_{k_n}$ contains infinitely many points from the sequence $A$, and
The diameter of $I_{k_n}$ is $<2^{-n}$.
Note that the existence of each $k_n$, and the sequence $(k_n)_{n\in\mathbb{N}}$, is provable without using choice: the entire construction is explicit.
Now let $b_n$ be the right endpoint of $I_{k_n}$; the sequence $(b_n)_{n\in\mathbb{N}}$ is a Cauchy sequence, hence has a limit $\beta$, and it's easy to check that $\beta$ is in fact a limit point for the original sequence $A$.
On the other hand, in a "less-concrete" situation (= no longer "well-orderably-approximable"), we often do need some choice principle. For example, it's consistent with ZF (= set theory without choice) that there is a poset with no infinite descending sequence which however is not well-founded, so your third example really does constitute a necessary use of a choice principle. Functional analysis and point-set topology also provide examples, as do some seemingly-basic set theoretic questions about $\mathbb{R}$ (for example, it's consistent with ZF that there is an infinite, Dedekind-finite set of real numbers).
But I would argue that there are vanishingly few examples in basic real analysis which actually need choice.