Theorem: Weierstrass Extreme Value Theorem

Let $f$ be a real function which is continuous in a closed real interval $\closedint a b$.
Then:
:$\exists x_M: \forall x \in \closedint a b: \map f {x_M} \ge \map f x$
:$\exists x_m: \forall x \in \closedint a b: \map f {x_m} \le \map f x$

Proof:
{{tidy}}
We will prove the case for $x_M$, the maximum.
The case for $x_m$, the minimum, is similar.
First it is shown that $\map f x$ is bounded above in the closed real interval $\closedint a b$.
{{AimForCont}} $\map f x$ has no upper bound.
Then:
:$\forall N \in \N: \exists x_N \in \closedint a b: \map f {x_N} > N$
Consider the sequence:
:$\sequence {x_N} \in \closedint a b$
$\sequence {x_N}$ is bounded:
:bounded above by $b$
:bounded below by $a$.
By the Bolzano-Weierstrass Theorem there exists a subsequence of $\sequence {x_N}$, call it $\sequence {g_n}$, which converges to a point in $\closedint a b$.
So, let $g_n \to d$ with $d \in \closedint a b$.
We have {{hypothesis}} that $f$ is continuous on $\closedint a b$
Hence by Continuity of Mapping between Metric Spaces by Convergent Sequence:
:$\ds \lim_{n \mathop \to \infty} \map f {g_n} = \map f d$
But by the Axiom of Archimedes, there exists $N_d \in \N$ such that:
:$N_d > \map f d$
By assumption, for every $N \ge N_d$:
:$x_N \ge N \ge N_d$
Therefore, there are at most $N_d$ terms of $x_N$ satisfying:
:$\size {x_N - \map f d} < N_d - \map f d$
But as $g_n$ is a subsequence of $x_N$, that contradicts the fact that:
:$\ds \lim_{n \mathop \to \infty} \map f {g_n} = \map f d$
{{qed|lemma}}
We have shown that:
:$\set {\map f x : x \in \closedint a b}$
is bounded above.
Therefore, by Least Upper Bound Property:
:$M = \sup_{x \in \closedint a b} \map f x$
It remains to be proved that:
:$\exists x_M \in \closedint a b : \map f {x_M} = M$
We will construct $\sequence {x_n}$ such that:
:$\forall n \in \N_{> 0}: M - \dfrac 1 n < \map f {x_n} \le M$
as follows:
Let $n \in \N_{> 0}$ be arbitrary.
Then, $\dfrac 1 n > 0$.
Therefore:
:$M - \dfrac 1 n < M$
Thus, by Characterizing Property of Supremum of Subset of Real Numbers:
:$\exists y_n \in f \closedint a b: M - \dfrac 1 n < y_n \le M$
That is:
:$\exists x_n \in \closedint a b: M - \dfrac 1 n < \map f {x_n} \le M$
by definition of image.
Therefore, $\sequence {x_n}_{n \in \N_{> 0}}$ satisfies:
:$\forall n \in \N_{> 0}: M - \dfrac 1 n < \map f {x_n} \le M$
{{qed|lemma}}
For every $n \in \N_{> 0}$:
:$\size {M - x_n} < \dfrac 1 n$
By Sequence of Reciprocals is Null Sequence, it follows that:
:$\ds \lim_{n \mathop \to \infty} x_n = M$
Consider $\sequence {x_n}$.
Because it is bounded as before, by Bolzano-Weierstrass Theorem there exists a subsequence:
:$\sequence {s_n}$
that converges.
Let it converge to $l$.
Because $\sequence {s_n} \in \closedint a b$ it follows that:
:$l \in \closedint a b$.
Finally, $\map f x$ is continuous in $\closedint a b$.
So, by Continuity of Mapping between Metric Spaces by Convergent Sequence:
:$\ds \lim_{n \mathop \to \infty} \map f {s_n} = \map f l$
But $\sequence {\map f {s_n} }$ is a subsequence of $\sequence {\map f {x_n} }$.
So, by Limit of Subsequence equals Limit of Real Sequence:
:$\ds \lim_{n \mathop \to \infty} \map f {s_n} = M$
Therefore:
:$\map f l = M$
{{qed}}