Was wondering if anyone could validate my proof that Axiom of Completeness (AoC) implies that the Bolzano-Weirestrass theorem must be true. I'm pretty confident on this one but as someone very new to proof-writing (I pretty much wrote my first formal proof last month) and "Pure Mathematics" I often feel like I might be missing something. I'll state a few assumptions and definitions at the outset. This is the answer to an excercise and prompt in S. Abbot's Understanding Analysis.
1.1 Axiom of Completeness: Every nonempty set of real numbers that is bounded above has a least upper bound. E.g for all nonempty real-numbered sets $A$, there exists some $\text{Sup(}A)$ (see next defininition)
1.2 Supremum/Least Upper Bound: The least upper bound of some set is denoted with $\text{Sup}A$. for some $ s = \text{Sup}A$ to exist, $s$ must have two properties. i) $s \ge a, a \in A$ and ii) $s\le b$ where $b$ is any upper bound on $A$.
1.2.1 (Lemma): if $ s = \text{Sup}A$, it is also equivalent to state that $s - a < \epsilon$ for any $\epsilon \in \mathbb{R}: \epsilon > 0$ Furthermore if we assume that $s\ge a, a \in A$ then this lemma is equivalent to saying $|s - a| < \epsilon$ since $s-a$ is always a positive number anyways.
1.3 Bolzano-Weierestrass Theorem (what we are trying to prove): Every bounded sequence contains a convergent subsequence.
Proof (AoC Implies Bolzano-Weierstrass):
Let $a_n$ be some bounded sequence and let
$$S = \{x \in \mathbb(R): x < \text{infinitely many terms in } a_n\}.$$ By definition, if we have some real number $x \in S$, since there must be infinitely many $a_n$ terms larger than it, then we can always find some term in $a_n$, $a_k$ that is larger than $x$. Furthermore, since $a_n$ is an infinite sequence, this $a_k$ also has an infinite amount of terms from $a_n$ larger than it, so this $a_k$ is also a member of $S$.
In general, for any $x \in S$, we can find some $a_k \in S$ that is larger than it.
Leave that there for now. Since we are allowed to assume AoC, and since $S$ is a bounded, nonempty sequence, $s = \text{sup}S$ must exist. By lemma 1.2.1, we can also say that $|s-x| < \epsilon$ where $x \in S$ and $\epsilon > 0$.
By our earlier logic, for any $x$ in $|s-x| < \epsilon$ we can find some $a_k$ larger than $x$, s.t that $|s-a_k| \le |s-x| < \epsilon$ which we can get $|s-a_k| < \epsilon$ from. If we define some infinite sequence $a_k$ where all elements in $a_k$ are from S and are obviously all terms from $a_n$, we have found some subsequence of $a_n$. Since $|s-a_k| < \epsilon$ is true (and obviously then $|a_k-s| < \epsilon$ is as well), notice that is the definition of convergence, and we have shown that in every bounded sequence there exists a convergent subsequence, which is what the Bolzano-Weierestrass Theorem claims.
$\blacksquare$
I would be super grateful if anyone could validate it! Thanks!