avewright/proofwiki-math huggingface dataset:
Theorem: Strictly Positive Rational Numbers under Multiplication form Countably Infinite Abelian Group

Let $\Q_{> 0}$ be the set of strictly positive rational numbers, i.e. $\Q_{> 0} = \set {x \in \Q: x > 0}$.
The structure $\struct {\Q_{> 0}, \times}$ is a countably infinite abelian group.

Proof:
From Strictly Positive Rational Numbers under Multiplication form Subgroup of Non-Zero Rational Numbers we have that $\struct {\Q_{> 0}, \times}$ is a subgroup of $\struct {\Q_{\ne 0}, \times}$, where $\Q_{\ne 0}$ is the set of rational numbers without zero: $\Q_{\ne 0} = \Q \setminus \set 0$.
From Subgroup of Abelian Group is Abelian it follows that $\struct {\Q_{> 0}, \times}$ is an abelian group.
From Positive Rational Numbers are Countably Infinite, it follows that $\struct {\Q_{> 0}, \times}$ is a countably infinite group.
{{qed}}
Theorem: Multinomial Theorem

Let $x_1, x_2, \ldots, x_k \in F$, where $F$ is a field.
Then:
:$\ds \paren {x_1 + x_2 + \cdots + x_m}^n = \sum_{k_1 \mathop + k_2 \mathop + \mathop \cdots \mathop + k_m \mathop = n} \binom n {k_1, k_2, \ldots, k_m} {x_1}^{k_1} {x_2}^{k_2} \cdots {x_m}^{k_m}$
where:
:$m \in \Z_{> 0}$ is a positive integer
:$n \in \Z_{\ge 0}$ is a non-negative integer
:$\dbinom n {k_1, k_2, \ldots, k_m} = \dfrac {n!} {k_1! \, k_2! \, \cdots k_m!}$ denotes a multinomial coefficient.
The sum is taken for all non-negative integers $k_1, k_2, \ldots, k_m$ such that $k_1 + k_2 + \cdots + k_m = n$, and with the understanding that wherever $0^0$ may appear it shall be considered to have a value of $1$.

Proof:
The proof proceeds by induction on $m$.
For each $m \in \N_{\ge 1}$, let $\map P m$ be the proposition:
:$\ds \forall n \in \N: \paren {x_1 + x_2 + \cdots + x_m}^n = \sum_{k_1 \mathop + k_2 \mathop + \mathop \cdots \mathop + k_m \mathop = n} \binom n {k_1, k_2, \ldots, k_m} {x_1}^{k_1} {x_2}^{k_2} \cdots {x_m}^{k_m}$
Theorem: Mapping is Constant iff Increasing and Decreasing

Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $\phi: \struct {S, \preceq_1} \to \struct {T, \preceq_2}$ be a mapping.
Then $\phi$ is a constant mapping {{iff}} $\phi$ is both increasing and decreasing.

Proof:
=== Necessary Condition ===
Suppose $\phi$ is a constant mapping.
Then:
: $\forall x, y \in S: \map \phi x = \map \phi y$
So:
: $\forall x, y \in S: \map \phi x \mathop{\preceq_2} \map \phi y$
: $\forall x, y \in S: \map \phi y \mathop{\preceq_2} \map \phi x$
and so $\phi$ is both increasing and decreasing.
{{qed|lemma}}
Theorem: Powers Drown Logarithms

Let $r \in \R_{>0}$ be a (strictly) positive real number.
Then:
:$\ds \lim_{x \mathop \to \infty} x^{-r} \ln x = 0$

Proof:
From Upper Bound of Natural Logarithm:
When $x > 1$:
: $\forall s \in \R: s > 0: \ln x \le \dfrac {x^s} s$
Given that $r > 0$, we can plug $s = \dfrac r 2$ in:
{{begin-eqn}}
{{eqn | l = x^{-r} \ln x
      | r = x^{-r/2} \paren {x^{-s} \ln x}
      | c = 
}}
{{eqn | o = \le
      | r = \frac {x^{-r/2} } s
      | c = 
}}
{{eqn | r = s \frac 1 {x^{r/2} }
      | c = 
}}
{{end-eqn}}
From Sequence of Powers of Reciprocals is Null Sequence:
:$\ds \lim_{x \mathop \to \infty} x^{-r} \frac 1 {x^{r/2} } = 0$
and so:
:$\ds \lim_{x \mathop \to \infty} x^{-r} \ln x = 0$
by the Squeeze Theorem for Real Sequences.
{{qed}}
Theorem: Equivalence of Well-Ordering Principle and Induction

The Well-Ordering Principle, the Principle of Finite Induction and the Principle of Complete Finite Induction are logically equivalent.
That is:
:Principle of Finite Induction: Given a subset $S \subseteq \N$ of the natural numbers which has these properties:
:: $0 \in S$
:: $n \in S \implies n + 1 \in S$
:then $S = \N$.
{{iff}}:
:Principle of Complete Finite Induction: Given a subset $S \subseteq \N$ of the natural numbers which has these properties:
:: $0 \in S$
:: $\set {0, 1, \ldots, n} \subseteq S \implies n + 1 \in S$
:then $S = \N$.
{{iff}}:
:Well-Ordering Principle: Every non-empty subset of $\N$ has a minimal element.

Proof:
To save space, we will refer to:
: The Well-Ordering Principle as '''WOP'''
: The Principle of Finite Induction as '''PFI'''
: The Principle of Complete Finite Induction as '''PCI'''.
Theorem: Lower Bound for Subset

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $L$ be a lower bound for $S$.
Let $\left({T, \preceq}\right)$ be a subset of $\left({S, \preceq}\right)$.
Then $L$ is a lower bound for $T$.

Proof:
By definition of lower bound:
:$\forall x \in S: L \preceq x$
But as $\forall y \in T: y \in S$ by definition of subset, it follows that:
:$\forall y \in T: L \preceq y$.
Hence the result, again by definition of lower bound.
{{qed}}
Theorem: Upper Bound for Subset

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $U$ be an upper bound for $S$.
Let $\left({T, \preceq}\right)$ be a subset of $\left({S, \preceq}\right)$.
Then $U$ is an upper bound for $T$.

Proof:
By definition of upper bound:
:$\forall x \in S: x \preceq U$
But as $\forall y \in T: y \in S$ by definition of subset, it follows that:
:$\forall y \in T: y \preceq U$.
Hence the result, again by definition of upper bound.
{{qed}}
Theorem: Common Divisor Divides GCD

Let $a, b \in \Z$ such that not both of $a$ and $b$ are zero.
Let $c$ be any common divisor of $a$ and $b$.
That is, let $c \in \Z: c \divides a, c \divides b$.
Then:
:$c \divides \gcd \set {a, b}$
where $\gcd \set {a, b}$ is the greatest common divisor of $a$ and $b$.

Proof:
Let $d = \gcd \set {a, b}$.
Then $d \divides a$ and $d \divides b$ by definition.
Then from Bézout's Identity, $\exists u, v \in \Z: d = u a + v b$.
From Common Divisor Divides Integer Combination, $c \divides a \land c \divides b \implies c \divides u a + v b$ for all $u, v \in \Z$.
Thus $c \divides d$.
{{qed}}
Theorem: Square Modulo 5

Let $x \in \Z$ be an integer.
Then one of the following holds:
{{begin-eqn}}
{{eqn | l = x^2
      | o = \equiv
      | r = 0 \pmod 5
      | c = 
}}
{{eqn | l = x^2
      | o = \equiv
      | r = 1 \pmod 5
      | c = 
}}
{{eqn | l = x^2
      | o = \equiv
      | r = 4 \pmod 5
      | c = 
}}
{{end-eqn}}

Proof:
Let $x$ be an integer.
Using Congruence of Powers throughout, we make use of $x \equiv y \pmod 5 \implies x^2 \equiv y^2 \pmod 5$.
There are five cases to consider:
: $x \equiv 0 \pmod 5$: we have $x^2 \equiv 0^2 \pmod 5 \equiv 0 \pmod 5$.
: $x \equiv 1 \pmod 5$: we have $x^2 \equiv 1^2 \pmod 5 \equiv 1 \pmod 5$.
: $x \equiv 2 \pmod 5$: we have $x^2 \equiv 2^2 \pmod 5 \equiv 4 \pmod 5$.
: $x \equiv 3 \pmod 5$: we have $x^2 \equiv 3^2 \pmod 5 \equiv 4 \pmod 5$.
: $x \equiv 4 \pmod 5$: we have $x^2 \equiv 4^2 \pmod 5 \equiv 1 \pmod 5$.
{{qed}}
Theorem: Square Modulo 3

Let $x \in \Z$ be an integer.
Then one of the following holds:
{{begin-eqn}}
{{eqn | l = x^2
      | o = \equiv
      | r = 0 \pmod 3
      | c = when $3 \divides x$
}}
{{eqn | l = x^2
      | o = \equiv
      | r = 1 \pmod 3
      | c = when $3 \nmid x$
}}
{{end-eqn}}
where:
:$\divides$ denotes divisibility
:$\nmid$ denotes non-divisibility.

Proof:
Let $x$ be an integer.
Using Congruence of Powers throughout, we make use of:
: $x \equiv y \pmod 3 \implies x^2 \equiv y^2 \pmod 3$
There are three cases to consider:
: $(1): \quad x \equiv 0 \pmod 3$: we have $x^2 \equiv 0^2 \pmod 3 \equiv 0 \pmod 3$
: $(2): \quad x \equiv 1 \pmod 3$: we have $x^2 \equiv 1^2 \pmod 3 \equiv 1 \pmod 3$
: $(3): \quad x \equiv 2 \pmod 3$: we have $x^2 \equiv 2^2 \pmod 3 \equiv 1 \pmod 3$
{{qed}}
Theorem: Additive Group of Integers is Countably Infinite Abelian Group

The set of integers under addition $\struct {\Z, +}$ forms a countably infinite abelian group.

Proof:
From Integers under Addition form Abelian Group, $\struct {\Z, +}$ is an abelian group.
From Integers are Countably Infinite, the set of integers can be placed in one-to-one correspondence with the set of natural numbers.
Hence by definition, the underlying set  of $\struct {\Z, +}$ is countably infinite.
{{qed}}
Theorem: Division Laws for Groups

Let $G$ be a group.
Let $a, b, x \in G$.
Then:
:$(1): \quad a x = b \iff x = a^{-1} b$
:$(2): \quad x a = b \iff x = b a^{-1}$

Proof:
All derivations can be achieved using applications of the group axioms:
Theorem: Center is Intersection of Centralizers

The center of a group is the intersection of all the centralizers of the elements of that group:
:$\ds \map Z G = \bigcap_{g \mathop \in G} \map {C_G} g$

Proof:
Denote $Z = \map Z G$ and $C = \ds \bigcap_{g \mathop \in G} \map {C_G} g$ for simplicity.
By definition of set equality, it suffices to prove $Z \subseteq C$ and $C \subseteq Z$.
Theorem: Group Homomorphism Preserves Identity

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
Let:
:$e_G$ be the identity of $G$
:$e_H$ be the identity of $H$.
Then:
:$\map \phi {e_G} = e_H$

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {e_G}
      | r = \map \phi {e_G \circ e_G}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \map \phi {e_G} * \map \phi {e_G}
      | c = {{Defof|Morphism Property}}
}}
{{end-eqn}}
That is:
{{begin-eqn}}
{{eqn | l = \map \phi {e_G} * e_H
      | r = \map \phi {e_G} * \map \phi {e_G}
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = e_H
      | r = \map \phi {e_G}
      | c = Cancellation Laws
}}
{{end-eqn}}
{{qed}}
Theorem: Group Homomorphism Preserves Identity

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
Let:
:$e_G$ be the identity of $G$
:$e_H$ be the identity of $H$.
Then:
:$\map \phi {e_G} = e_H$

Proof:
A direct application of Homomorphism to Group Preserves Identity.
{{qed}}
Theorem: Group Homomorphism Preserves Identity

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to \struct {H, *}$ be a group homomorphism.
Let:
:$e_G$ be the identity of $G$
:$e_H$ be the identity of $H$.
Then:
:$\map \phi {e_G} = e_H$

Proof:
From Group Homomorphism of Product with Inverse, we have:
:$\forall x, y \in G: \map \phi {x \circ y^{-1} } = \map \phi x * \paren {\map \phi y}^{-1}$
Putting $x = y$ we have:
{{begin-eqn}}
{{eqn | l = \map \phi {e_G}
      | r = \map \phi {x \circ x^{-1} }
      | c = 
}}
{{eqn | r = \map \phi x * \paren {\map \phi x}^{-1}
      | c = 
}}
{{eqn | r = e_H
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Group Homomorphism Preserves Inverses

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to\struct {H, *}$ be a group homomorphism.
Let:
:$e_G$ be the identity of $G$
:$e_H$ be the identity of $H$
Then:
:$\forall x \in G: \map \phi {x^{-1} } = \paren {\map \phi x}^{-1}$

Proof:
Let $x \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi x * \map \phi {x^{-1} }
      | r = \map \phi {x \circ x^{-1} }
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = \map \phi {e_G}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = e_H
      | c = Group Homomorphism Preserves Identity
}}
{{end-eqn}}
So, by definition, $\map \phi {x^{-1} }$ is the right inverse of $\map \phi x$.
{{qed|lemma}}
Similarly:
{{begin-eqn}}
{{eqn | l = \map \phi {x^{-1} } * \map \phi x
      | r = \map \phi {x^{-1} \circ x}
      | c = {{Defof|Group Homomorphism}}
}}
{{eqn | r = \map \phi {e_G}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = e_H
      | c = Group Homomorphism Preserves Identity
}}
{{end-eqn}}
So, again by definition, $\map \phi {x^{-1} }$ is the left inverse of $\map \phi x$.
{{qed|lemma}}
Finally, as $\map \phi {x^{-1} }$ is both:
:a left inverse of $\map \phi x$
and:
:a right inverse of $\map \phi x$
it is by definition an inverse.
From Inverse in Group is Unique, $\map \phi {x^{-1} }$ is the only such element.
Hence the result.
{{qed}}
Theorem: Group Homomorphism Preserves Inverses

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to\struct {H, *}$ be a group homomorphism.
Let:
:$e_G$ be the identity of $G$
:$e_H$ be the identity of $H$
Then:
:$\forall x \in G: \map \phi {x^{-1} } = \paren {\map \phi x}^{-1}$

Proof:
A direct application of Homomorphism to Group Preserves Inverses.
{{qed}}
Theorem: Group Homomorphism Preserves Inverses

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: \struct {G, \circ} \to\struct {H, *}$ be a group homomorphism.
Let:
:$e_G$ be the identity of $G$
:$e_H$ be the identity of $H$
Then:
:$\forall x \in G: \map \phi {x^{-1} } = \paren {\map \phi x}^{-1}$

Proof:
From Group Homomorphism of Product with Inverse, we have:
:$\forall x, y \in G: \map \phi {x \circ y^{-1} } = \map \phi x * \paren {\map \phi y}^{-1}$
Putting $x = e_G$ and $y = x$ we have:
{{begin-eqn}}
{{eqn | l = \map \phi {x^{-1} }
      | r = \map \phi {e_G \circ x^{-1} }
      | c = 
}}
{{eqn | r = \map \phi {e_G} * \paren {\map \phi x}^{-1}
      | c = 
}}
{{eqn | r = e_H * \paren {\map \phi x}^{-1}
      | c = Group Homomorphism Preserves Identity
}}
{{eqn | r = \paren {\map \phi x}^{-1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Subset Product with Normal Subgroup is Subgroup

Let $G$ be a group whose identity is $e$.
Let:
:$(1): \quad H$ be a subgroup of $G$
:$(2): \quad N$ be a normal subgroup of $G$.
Let $H N$ denote subset product.
Then $H N$ and $N H$ are both subgroups of $G$.

Proof:
It is clear that $e \in N H$, so $N H \ne \O$.
Suppose $n_1, n_2 \in N$ and $h_1, h_2 \in H$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {n_1 h_1} \paren {n_2 h_2}
      | r = n_1 \paren {h_1 n_2 h_1^{-1} h_1} h_2
}}
{{eqn | r = n_1 \paren {h_1 n_2 h_1^{-1} } \paren {h_1 h_2}
}}
{{end-eqn}}
Since $N$ is normal in $G$:
:$\exists n \in N: n = h_1 n_2 h_1^{-1}$
Thus:
{{begin-eqn}}
{{eqn | l = \paren {n_1 h_1} \paren {n_2 h_2}
      | r = \paren {n_1 n} \paren {h_1 h_2}
}}
{{eqn | o = \in
      | r = N H
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \paren {n_1 h_1}^{-1}
      | r = h_1^{-1} n_1^{-1}
}}
{{eqn | r = \paren {h_1^{-1} n_1^{-1} h_1} h_1^{-1}
}}
{{eqn | o = \in
      | r = N H
}}
{{end-eqn}}
so from the Two-Step Subgroup Test, $N H$ is a subgroup of $G$.
The fact that $N H = H N$ follows from Subset Product of Subgroups.
{{qed}}
Theorem: Subset Product with Normal Subgroup is Subgroup

Let $G$ be a group whose identity is $e$.
Let:
:$(1): \quad H$ be a subgroup of $G$
:$(2): \quad N$ be a normal subgroup of $G$.
Let $H N$ denote subset product.
Then $H N$ and $N H$ are both subgroups of $G$.

Proof:
Consider the subset product $N H$.
We have that:
{{begin-eqn}}
{{eqn | l = N H
      | r = \set {n h : n \in N , h \in H}
      | c = {{Defof|Subset Product}}
}}
{{eqn | r = \bigcup_{h \mathop \in H} \set {n h : n \in N}
      | c = {{Defof|Union of Family}}
}}
{{eqn | r = \bigcup_{h \mathop \in H} N h
      | c = {{Defof|Left Coset}}
}}
{{eqn | r = \bigcup_{h \mathop \in H} h N
      | c = $N$ is normal
}}
{{eqn | r = \bigcup_{h \mathop \in H} \set {h n : n \in N}
      | c = {{Defof|Right Coset}}
}}
{{eqn | r = \set {h n : n \in N , h \in H}
      | c = {{Defof|Union of Family}}
}}
{{eqn | r = H N
      | c = {{Defof|Subset Product}}
}}
{{end-eqn}}
Therefore, $N$ and $H$ are permutable.
The result follows from Subset Product of Subgroups.
{{qed}}
Theorem: Ring Homomorphism Preserves Zero

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring homomorphism.
Let:
:$0_{R_1}$ be the zero of $R_1$
:$0_{R_2}$ be the zero of $R_2$.
Then:
:$\map \phi {0_{R_1} } = 0_{R_2}$

Proof:
By definition, if $\struct {R_1, +_1, \circ_1}$ and $\struct {R_2, +_2, \circ_2}$ are rings then $\struct {R_1, +_1}$ and $\struct {R_2, +_2}$ are groups.
Again by definition:
:the zero of $\struct {R_1, +_1, \circ_1}$ is the identity of $\struct {R_1, +_1}$
:the zero of $\struct {R_2, +_2, \circ_2}$ is the identity of $\struct {R_2, +_2}$.
The result follows from Group Homomorphism Preserves Identity.
{{Qed}}
Theorem: Image of Set Difference under Mapping

Let $f: S \to T$ be a mapping.
The set difference of the images of two subsets of $S$ is a subset of the image of the set difference.
That is:
Let $S_1$ and $S_2$ be subsets of $S$.
Then:
:$f \sqbrk {S_1} \setminus f \sqbrk {S_2} \subseteq f \sqbrk {S_1 \setminus S_2}$
where $\setminus$ denotes set difference.

Proof:
As $f$, being a mapping, is also a relation, we can apply Image of Set Difference under Relation:
:$\RR \sqbrk {S_1} \setminus \RR \sqbrk {S_2} \subseteq \RR \sqbrk {S_1 \setminus S_2}$
{{qed}}
Theorem: Image of Set Difference under Mapping

Let $f: S \to T$ be a mapping.
The set difference of the images of two subsets of $S$ is a subset of the image of the set difference.
That is:
Let $S_1$ and $S_2$ be subsets of $S$.
Then:
:$f \sqbrk {S_1} \setminus f \sqbrk {S_2} \subseteq f \sqbrk {S_1 \setminus S_2}$
where $\setminus$ denotes set difference.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = f \sqbrk {S_1} \setminus f \sqbrk {S_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in {S_1}: x \notin {S_2}
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in {S_1} \setminus {S_2}
      | l = \tuple {x, y}
      | o = \in
      | r = f
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = f \sqbrk {S_1 \setminus S_2}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Convergence by Multiple of Error Term

Let $\sequence {s_n}$ be a real sequence.
Suppose that $\exists \epsilon \in \R, \epsilon > 0$ such that:
:$\exists N \in \N: \forall n \ge N: \size {s_n - l} < K \epsilon$
for any $K \in \R, K > 0$, independent of both $\epsilon$ and $N$.
Then $\sequence {s_n}$ converges to $l$.

Proof:
Let $\epsilon > 0$.
Then $\dfrac \epsilon K > 0$.
If the condition holds as stated, then:
:$\exists N \in \N: \forall n \ge N: \size {s_n - l} < K \paren {\dfrac \epsilon K}$
Hence the result by definition of a convergent sequence.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers

Let $\sequence {x_n}$ be a sequence in $\R$.
Then $\sequence {x_n}$ is a Cauchy sequence {{iff}} $\sequence {x_n}$ is convergent.

Proof:
=== Necessary Condition ===
{{:Cauchy's Convergence Criterion/Real Numbers/Necessary Condition}}{{qed|lemma}}
Theorem: Cauchy's Convergence Criterion/Real Numbers

Let $\sequence {x_n}$ be a sequence in $\R$.
Then $\sequence {x_n}$ is a Cauchy sequence {{iff}} $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {x_n}$ be convergent.
Let $\struct {\R, d}$ be the metric space formed from $\R$ and the usual (Euclidean) metric:
:$\map d {x_1, x_2} = \size {x_1 - x_2}$
where $\size x$ is the absolute value of $x$.
This is proven to be a metric space in Real Number Line is Metric Space.
From Convergent Sequence in Metric Space is Cauchy Sequence, we have that every convergent sequence in a metric space is a Cauchy sequence.
Hence $\sequence {x_n}$ is a Cauchy sequence.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers

Let $\sequence {x_n}$ be a sequence in $\R$.
Then $\sequence {x_n}$ is a Cauchy sequence {{iff}} $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {x_n}$ be a sequence in $\R$ that converges to the limit $l \in \R$.
Let $\epsilon > 0$. 
Then also $\dfrac \epsilon 2 > 0$.
Because $\sequence {x_n}$ converges to $l$, we have:
:$\exists N: \forall n > N: \size {x_n - l} < \dfrac \epsilon 2$
So if $m > N$ and $n > N$, then:
{{begin-eqn}}
{{eqn | l = \size {x_n - x_m}
      | r = \size {x_n - l + l - x_m}
}}
{{eqn | o = \le
      | r = \size {x_n - l} + \size {l - x_m}
      | c = Triangle Inequality
}}
{{eqn | o = <
      | r = \frac \epsilon 2 + \frac \epsilon 2
      | c = by choice of $N$
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Thus $\sequence {x_n}$ is a Cauchy sequence.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers

Let $\sequence {x_n}$ be a sequence in $\R$.
Then $\sequence {x_n}$ is a Cauchy sequence {{iff}} $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {a_n}$ be a Cauchy sequence in $\R$.
We have the result Real Number Line is Metric Space.
Hence by Convergent Subsequence of Cauchy Sequence, it is sufficient to show that $\sequence {a_n}$ has a convergent subsequence.
Since $\sequence {a_n}$ is Cauchy, by Real Cauchy Sequence is Bounded, it is also bounded.
By the Bolzano-Weierstrass Theorem, $\sequence {a_n}$ has a convergent subsequence.
Hence the result.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers

Let $\sequence {x_n}$ be a sequence in $\R$.
Then $\sequence {x_n}$ is a Cauchy sequence {{iff}} $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {a_n}$ be a Cauchy sequence in $\R$.
By Real Cauchy Sequence is Bounded, $\sequence {a_n}$ is bounded.
By the Bolzano-Weierstrass Theorem, $\sequence {a_n}$ has a convergent subsequence $\sequence {a_{n_r} }$.
Let $a_{n_r} \to l$ as $r \to \infty$.
It is to be shown that $a_n \to l$ as $n \to \infty$.
Let $\epsilon \in \R_{>0}$ be a (strictly) positive real number.
Then $\dfrac \epsilon 2 > 0$.
Hence:
:$(1): \quad \exists R \in \R: \forall r > R: \size {a_{n_r} - l} < \dfrac \epsilon 2$
We have that $\sequence {a_n}$ is a Cauchy sequence.
Hence:
:$(2): \quad \exists N \in \R: \forall m > N, n > N: \size {x_m - x_n} \le \dfrac \epsilon 2$
Let $n > N$.
Let $r \in \N$ be sufficiently large that:
:$n_r > N$
and:
:$r > R$
Then $(1)$ is satisfied, and $(2)$ is satisfied with $m = n_r$.
So:
{{begin-eqn}}
{{eqn | q = \forall n > N
      | l = \size {a_n - l}
      | r = \size {a_n - a_{n_r} + a_{n_r} - l}
      | c = 
}}
{{eqn | o = \le
      | r = \size {a_n - a_{n_r} } + \size{a_{n_r} - l}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = <
      | r = \dfrac \epsilon 2 + \dfrac \epsilon 2
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
So, given $\epsilon > 0$, we have found $n \in \R$ such that:
:$\forall n > N: \size {a_n - l} < \epsilon$
Thus:
:$x_n \to l$ as $n \to \infty$.
{{qed}}
Theorem: Cauchy's Convergence Criterion/Real Numbers

Let $\sequence {x_n}$ be a sequence in $\R$.
Then $\sequence {x_n}$ is a Cauchy sequence {{iff}} $\sequence {x_n}$ is convergent.

Proof:
Let $\sequence {a_n}$ be a Cauchy sequence in $\R$.
By Real Cauchy Sequence is Bounded, $\sequence {a_n}$ is bounded.
Thus $\sequence {a_n}$ is both bounded above and bounded below.
Let us create a monotone subsequence $\sequence {b_n}$ of $\sequence {a_n}$ using the following construction:
For each $m \in \N$, let $S_m$ denote the set of elements of $\sequence {a_n}$ from $m$ onwards:
:$S_m = \set {a_n: n \ge m}$
From Real Cauchy Sequence is Bounded, we have that $S_m$ is also bounded.
Hence, by the Continuum Property, $\sup S_m$ exists.
Let $b_m := \sup S_m$.
Because $S_{m + 1} \subseteq S_m$, it follows from Supremum of Set of Real Numbers is at least Supremum of Subset that:
:$\sup S_{m + 1} \le \sup S_m$
Thus $\sequence {b_m}$ is decreasing.
By definition of $b_m$, we also have that:
:$b_m \ge a_m$
So, as $\sequence {a_n}$ is bounded below, so is $\sequence {b_m}$.
So, by the Monotone Convergence Theorem (Real Analysis), $\sequence {b_m}$ is convergent.
Let $\sequence {b_m}$ converge to $l$.
Let $\epsilon \in \R_{>0}$ be arbitrary.
We have that $\sequence {a_n}$ is a Cauchy sequence in $\R$.
We also have from Subsequence of Real Cauchy Sequence is Cauchy that $\sequence {b_n}$ is also a Cauchy sequence in $\R$.
Then there exists:
:$N_1 \in \N$ such that $\size {a_m - a_n} < \epsilon$ for $m, n \ge N_1$
:$N_2 \in \N$ such that $\size {l - b_n} < \epsilon$ for $m \ge N_2$
Let $N = \max \set {N_1, N_2}$.
By definition of $b_N$, we have that $b_N - \epsilon$ is not an upper bound of $S_N = \set {a_n: n \ge N}$.
Thus there exists $M \ge N$ such that $a_M > b_N - \epsilon$.
We note also that $a_M \le b_N$ because $b_N$ is an upper bound for $S_N$.
Now let $n \ge N$.
We have that:
{{begin-eqn}}
{{eqn | l = \size {a_n - l}
      | r = \size {a_n - a_M + a_M - b_N + b_N - l}
      | c = 
}}
{{eqn | o = \le
      | r = \size {a_n - a_M} + \size {a_M - b_N} + \size {b_N - l}
      | c = Triangle Inequality
}}
{{eqn | o = <
      | r = 3 \epsilon
      | c = 
}}
{{end-eqn}}
Hence by Convergence by Multiple of Error Term we have that $\sequence {a_n}$ converges to $l$.
{{qed}}