avewright/proofwiki-math huggingface dataset:
Theorem: Cardinal Product Equal to Maximum

Let $S$ and $T$ be sets that are equinumerous to their cardinal number.
Let $\card S$ denote the cardinal number of $S$.
Suppose $S$ is infinite.
Suppose $T > 0$.
Then:
:$\card {S \times T} = \map \max {\card S, \card T}$

Proof:
Let $x$ denote $\map \max {\card S, \card T}$.
Then by Cartesian Product Preserves Cardinality:
:$S \times T \sim \card S \times \card T$
Let $f: S \times T \to \card S \times \card T$ be a bijection.
It follows that $f: S \times T \to x \times x$ is an injection.
Hence:
{{begin-eqn}}
{{eqn | l = \card {S \times T}
      | o = \le
      | r = \card {x \times x}
      | c = Injection iff Cardinal Inequality
}}
{{eqn | r = \card x
      | c = Non-Finite Cardinal is equal to Cardinal Product
}}
{{eqn | o = \le
      | r = x
      | c = Cardinal Number Less than Ordinal: Corollary
}}
{{end-eqn}}
Therefore:
:$\card {S \times T} \le x$
{{qed|lemma}}
Conversely:
:$x = \card S$ if $\card T \le \card S$
and:
:$x = \card T$ if $\card S \le \card T$
By Relation between Two Ordinals:
:$x = \card S$ or $x = \card T$
It follows by Set Less than Cardinal Product that:
:$x \le \card {S \times T}$
{{qed|lemma}}
Combining the two lemmas, it follows that:
:$x = \card {S \times T}$
{{qed}}
Theorem: Cardinal of Union Equal to Maximum

Let $S$ and $T$ be sets that are equinumerous to their cardinal number.
Let $\card S$ denote the cardinal number of $S$.
Suppose $S$ is infinite.
Then:
:$\card {S \cup T} = \map \max {\card S, \card T}$

Proof:
Let $x$ denote $\map \max {\card S, \card T}$.
$x = \card S$ if $\card T \le \card S$
$x = \card T$ if $\card S \le \card T$
By Relation between Two Ordinals:
:$x = \card S$ or $x = \card T$
In either case, it follows by Subset of Union that:
:$x \le \card {S \cup T}$
{{qed|lemma}}
If $\card T  = 1$ or $\card T = 0$, it follows that $\card {S \cup T} = \card S = x$ by the definition of an infinite set.
If $1 < \card T$, then $\card {S \cup T} \le \card {S \times T}$ by Cardinal of Union Less than Cardinal of Cartesian Product.
But by Cardinal Product Equal to Maximum, it follows that $\card {S \cup T} \le x$.
{{qed|lemma}}
Combining the two lemmas, it follows that $x = \card {S \cup T}$
{{qed}}
Theorem: Class of All Cardinals is Subclass of Class of All Ordinals

Let $\NN$ denote the class of all cardinals.
Let $\On$ denote the class of all ordinals.
Then:
:$\NN \subseteq \On$

Proof:
By definition of the class of all cardinals:
:$\NN = \set {x \in \On: \exists y: x = \card y}$
Every element of $\NN$ is thus an element of $\On$.
{{qed}}
Theorem: Cardinal of Cardinal Equal to Cardinal/Corollary

Let $\NN$ denote the class of all cardinal numbers.
Let $x$ be an ordinal.
Then:
:$x \in \NN \iff x = \card x$

Proof:
=== Necessary Condition ===
Suppose $x = \card x$.
Then $x = \card y$ for some $y$ by Existential Generalisation.
By definition of class of all cardinals:
:$\NN = \set {x \in \On: \exists y: x = \card y}$
It follows that $x \in \NN$.
{{qed|lemma}}
Theorem: Class of All Cardinals Contains Minimally Inductive Set

Let $\NN$ denote the class of all cardinal numbers.
Then:
:$\omega \subseteq \NN$
where $\omega$ denotes the minimally inductive set.

Proof:
Suppose $n \in \omega$.
By Cardinal of Finite Ordinal, $n = \card n$.
By Cardinal of Cardinal Equal to Cardinal/Corollary, $n \in \NN$.
{{qed}}
Theorem: Cardinal Equal to Collection of All Dominated Ordinals

Let $S$ be a set.
Let $\preccurlyeq$ denote the dominance relation.
Let $\On$ denote the class of all ordinals.
Let $x = \set {y \in \On: y \preccurlyeq S}$
Then:
{{begin-itemize}}
{{item|(1):|$x$ is an element of the class of all cardinals}}
{{item|(2):|There is no injection $f$ such that $f : x \to S$}}
{{end-itemize}}

Proof:
=== $x$ is an ordinal ===
$x$ is clearly a subset of the class of all ordinals.
Moreover, suppose $y \in x$ and $z \in y$.
Then $z \subseteq y$ by the fact that $y$ is an ordinal.
$y \in x$ means that $f : y \to S$ for some injective mapping $f$ by the definition of dominance.
But then, $f \restriction_z : z \to S$ is also an injection by Restriction of Injection is Injection.
Thus, $z \in x$ by the definition of $x$, so $x$ is transitive.
Therefore, $x$ is an ordinal, since it is a transitive subset of the ordinal class.
{{qed|lemma}}
Theorem: Class of All Cardinals is Proper Class

The class $\NN$ of all cardinal numbers is a proper class.

Proof:
{{AimForCont}} $\NN$ is a small class.
By Class of All Cardinals is Subclass of Class of All Ordinals:
:$\NN \subseteq \On$
Therefore, $\bigcup \NN$ is an ordinal by Union of Set of Ordinals is Ordinal.
{{mistake|The above theorem has been handled only for a set of ordinals, not a class}}
Take $x = \set {y \in \On: y \preccurlyeq \bigcup \NN}$.
By Cardinal Equal to Collection of All Dominated Ordinals, $x$ is a cardinal number and there is no injection $f: x \to \bigcup \NN$.
But since $x$ is a cardinal number, $x \in \NN$, so $x \subseteq \bigcup \NN$ by Set is Subset of Union.
Therefore, the identity mapping $I_x: x \to \bigcup \NN$ is an injection.
This is a contradiction.
Therefore by Proof by Contradiction $\NN$ is not a small class.
{{qed}}
Theorem: Class of Infinite Cardinals is Proper Class

The class of infinite cardinals $\NN’$ is a proper class.

Proof:
{{AimForCont}} $\NN'$ is a small class.
By Union of Small Classes is Small, $\NN’ \cup \omega$ is a small class.
By definition of the class of infinite cardinals, $\NN \subseteq \NN' \cup \omega$.
But by Axiom of Subsets Equivalents, this means that $\NN$ is a small class.
This contradicts Class of All Cardinals is Proper Class.
Therefore, $\NN’$ is not a small class.
{{qed}}
Theorem: Ordinal in Aleph iff Cardinal in Aleph

Let $x$ and $y$ be ordinals.
Then:
:$x \in \aleph_y \iff \card x \in \aleph_y$
where $\aleph$ denotes the aleph mapping.

Proof:
By the definition of the aleph mapping, $\aleph_y$ is an element of the class of infinite cardinals.
By Cardinal Inequality implies Ordinal Inequality, it follows that:
:$x \in \aleph_y \iff \card x \in \aleph_y$
{{qed}}
Theorem: Aleph Product is Aleph

Let $x$ be an ordinal.
Then:
:$\left|{\aleph_x \times \aleph_x}\right| = \aleph_x$
where $\aleph$ denotes the aleph mapping.

Proof:
{{begin-eqn}}
{{eqn | l = \left\vert{\aleph_x \times \aleph_x }\right\vert
      | r = \left\vert{\aleph_x}\right\vert
      | c = Non-Finite Cardinal is equal to Cardinal Product
}}
{{eqn | r = \aleph_x
      | c = Aleph is Infinite Cardinal
}}
{{end-eqn}}
{{qed}}
Theorem: Aleph is Infinite Cardinal

Let $x$ be an ordinal.
Then $\aleph_x$ is an infinite cardinal where $\aleph$ denotes the aleph mapping.

Proof:
Let $\On$ denote the class of all ordinals.
By definition of the aleph mapping:
:$\aleph: \On \to \NN'$
where $\NN'$ denotes the class of infinite cardinals.
The theorem statement is an immediate consequence of this fact.
{{qed}}
Category:Aleph Mapping
fw7gnjchle5si1169w9p1j8nfp5fjpi
Theorem: Surjection from Aleph to Ordinal

Let $x$ and $y$ be ordinals.
Suppose that:
:$0 < y < \aleph_{x+1}$
Then there is a surjection:
:$f : \aleph_x \to y$

Proof:
:$y < \aleph_{x+1}$, then $y < \aleph_x \lor y \sim \aleph_x$ by Ordinal Less than Successor Aleph.
In either case, $\left|{ y }\right| \le \aleph_x$ by Ordinal in Aleph iff Cardinal in Aleph and Equivalent Sets have Equal Cardinal Numbers.
The existence of the surjection follows from Surjection iff Cardinal Inequality.
{{qed}}
Theorem: Ordinal Less than Successor Aleph

Let $x$ and $y$ be ordinals.
Then:
:$y < \aleph_{x + 1} \iff y < \aleph_x \lor y \sim \aleph_x$

Proof:
=== Sufficient Condition ===
{{begin-eqn}}
{{eqn|l = y
     |o = <
     |r = \aleph_{x + 1}
     |c = 
}}
{{eqn|ll= \leadsto
     |l = \card y
     |o = <
     |r = \aleph_{x + 1}
     |c = Ordinal in Aleph iff Cardinal in Aleph
}}
{{end-eqn}}
But $\card y$ is a cardinal number, so it is either finite or an element of the class of infinite cardinala.
It is a finite set {{iff}} $y \in \omega$ by Ordinal is Finite iff Natural Number.
If $y \in \omega$, then $y \in \aleph_x$ since $\aleph_x$ is an infinite set by Aleph is Infinite.
If it is an element of the infinite cardinal class, then $y = \aleph_z$ for some ordinal $z$ by the definition of the aleph mapping.
This means that:
{{begin-eqn}}
{{eqn | l = \aleph_z
      | o = <
      | r = \aleph_{x + 1}
      | c = {{Hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = z
      | o = <
      | r = x + 1
      | c = since $\aleph$ is an order isomorphism
}}
{{eqn | ll= \leadsto
      | l = z < x
      | o = \lor
      | r = z = x
      | c = {{Defof|Successor Set}}
}}
{{end-eqn}}
Theorem: Aleph is Infinite

Let $x$ be an ordinal.
:$\aleph_x \ge \omega$
where:
:$\aleph$ denotes the aleph mapping
:$\omega$ denotes the minimally inductive set.

Proof:
Since $0 \le x$, it follows that $\aleph_0 \le \aleph_x$ by definition of the aleph mapping.
But $\aleph_0 = \omega$ by Aleph-Null.
Therefore, $\omega \le \aleph_x$.
{{qed}}
Category:Aleph Mapping
p6e8lhletljz11ngl6ronn8dye4jd29
Theorem: Aleph-Null

Let $\omega$ denote the minimally inductive set.
:$\omega = \aleph_0$
where $\aleph$ denotes the aleph mapping.

Proof:
For all $n \in \omega$, $n \notin \NN'$ by the definition of the class of infinite cardinals.
Therefore, $\omega \le \aleph_0$.
{{qed|lemma}}
Moreover, $\omega \in \NN'$ by Minimally Inductive Set is Infinite Cardinal.
Therefore, $\aleph_x = \omega$ for some ordinal $x$.
It follows that $\aleph_0 \le \aleph_x$ since $0 \le x$ and the definition of the aleph mapping, so $\aleph_0 \le \omega$.
Thus, $\aleph_0 = \omega$.
{{qed}}
Category:Aleph Mapping
em41xt36mwwc8qqjdzxbonwv349dr9l
Theorem: Minimally Inductive Set is Infinite Cardinal

$\omega$, the minimally inductive set, is an element of the class of infinite cardinals $\NN'$.

Proof:
By {{Corollary|Cardinal Number Less than Ordinal}}:
:$\card \omega \le \omega$
Moreover, for any $n \in \omega$, by Cardinal of Finite Ordinal:
:$\card n < \card {n + 1} \le \card \omega$
Thus by Cardinal of Finite Ordinal:
:$n \in \card \omega$
Therefore:
:$\omega = \card \omega$
By {{Corollary|Cardinal of Cardinal Equal to Cardinal}}:
:$\omega \in \NN'$
{{qed}}
Category:Cardinals
Category:Minimally Inductive Set
ktxwz4pcdcui1vidbrmhmd52fpf77ob
Theorem: Set of All Mappings is Small Class

Let $S$ and $T$ be small classes.
It follows that the set of all mappings $S^T$ is a small class.

Proof:
The set of all mappings $S^T$ is equal to the collection of all mappings $f : S \to T$.
Each of these mappings $f$ is a subset of $S \times T$.
Thus, $S^T \subseteq \powerset {S \times T}$.
Therefore, by Cartesian Product is Small and the axiom of powers, $S^T$ is a small class.
{{qed}}
Theorem: Set of All Mappings of Cartesian Product

Let $R$, $S$, and $T$ be sets.
Then:
:$R^{S \times T} \sim \paren {R^S}^T$
where $R^{S \times T}$ denotes the set of all mappings from $S \times T$ to $R$.

Proof:
Define the mapping $F: \paren {R^S}^T \to R^{S \times T}$ as follows:
:$\map {\map F f} {x, y} = \map {\paren {\map f x} } y$ for all $x \in S , y \in T$.
Suppose $\map F {f_1} = \map F {f_2}$.
Then $\map {\paren {\map {f_1} x} } y = \map {\paren {\map {f_2} x} } y$ for all $x \in S , y \in T$ by the definition of $F$.
Therefore, $\map {f_1} x = \map {f_2} x$ and $f_1 = f_2$ by Equality of Mappings.
It follows that $F$ is an injection.
Take any $g \in R^{S \times T}$.
Define a function $f$ as $\map {\paren {\map f x} } y = \map g {x, y}$.
It follows that:
{{begin-eqn}}
{{eqn | l = \map {\map F f} {x, y}
      | r = \map {\paren {\map f x} } y
      | c = Definition of $F$
}}
{{eqn | r = \map g {x, y}
      | c = Definition of $f$
}}
{{end-eqn}}
Therefore, $F$ is a surjection.
Thus, $F$ is a bijection.
It follows that $ R^{S \times T} \sim \paren {R^S}^T$ by the definition of set equivalence.
{{qed}}
Theorem: Covariant Hom Functor is Functor

Let $\mathbf{Set}$ be the category of sets.
Let $\mathbf C$ be a locally small category.
Let $C \in \mathbf C_0$ be an object of $\mathbf C$.
Let $\operatorname{Hom}_\mathbf C \paren {C, \cdot}: \mathbf C \to \mathbf{Set}$ be the covariant hom functor based at $C$.
Then $\operatorname{Hom}_\mathbf C \paren {C, \cdot}$ is a functor.

Proof:
For brevity and readability, let us write $\operatorname{Hom}$ for $\operatorname{Hom}_\mathbf C$.
For any object $D$ of $\mathbf C$ and morphism $f: C \to D \in \operatorname{Hom} \paren {C, D}$, we have:
:$\operatorname{Hom} \paren {C, \operatorname{id}_D} \paren f = \operatorname{id}_D \circ f = f$
and so:
:$\operatorname{Hom} \paren {C, \operatorname{id}_D} = \operatorname{id}_{\operatorname{Hom} \paren {C, D} }$
Thus:
:$\operatorname{Hom} \paren {C, \cdot}$ preserves identity morphisms
For composable morphisms $g$ and $f$ of $\mathbf C$ we furthermore have:
{{begin-eqn}}
{{eqn | l = \operatorname{Hom} \paren {C, g \circ f} \paren x
      | r = \paren {g \circ f} \circ x
}}
{{eqn | r = g \circ \paren {f \circ x}
      | c = Composition of morphisms is associative
}}
{{eqn | r = \operatorname{Hom} \paren {C, g} \circ \operatorname{Hom} \paren {C, f} \paren x
}}
{{end-eqn}}
for any $x \in \operatorname{Hom} \paren {C, \operatorname{dom} f}$ composable with $f$.
Hence the result, by Equality of Mappings.
{{qed}}
Theorem: Inverse Morphism is Unique

Let $\mathbf C$ be a metacategory.
Let $f: C \to D$ be an isomorphism of $\mathbf C$.
Then $f$ admits a unique inverse morphism $g: D \to C$.

Proof:
Since $f$ is an isomorphism, it admits at least one inverse morphism.
Now let $g, g': D \to C$ be two inverse morphisms for $f$.
Then:
{{begin-eqn}}
{{eqn|l = g
     |r = g \circ \operatorname{id}_D
     |c = Axiom $(C2)$ for metacategories
}}
{{eqn|r = g \circ \left({f \circ g'}\right)
     |c = $g'$ is an inverse morphism for $f$
}}
{{eqn|r = \left({g \circ f}\right) \circ g'
     |c = Axiom $(C3)$ for metacategories
}}
{{eqn|r = {\operatorname{id}_C} \circ g'
     |c = $g$ is an inverse morphism for $f$
}}
{{eqn|r = g'
     |c = Axiom $(C2)$ for metacategories
}}
{{end-eqn}}
In conclusion, $g = g'$.
Hence the result.
{{qed}}
Theorem: Cofinal Ordinal Relation is Reflexive

Let $x$ be an ordinal.
Then $x$ is cofinal to itself.
That is:
:$\operatorname{cof} \left({x, x}\right)$

Proof:
{{MissingLinks|to $\le$, mostly. Some of the results have their own pages already}}
Each of the conditions for cofinal ordinals shall be verified:
:$x \le x$ follows by Set is Subset of Itself.
The mapping $f: x \to x$ can simply be the identity mapping $I_x$:
:$I_x: x \to x$
Moreover, $a < b \implies I_x \left({a}\right) < I_x \left({b}\right)$ by the definition of the identity mapping.
Therefore:
:$I_x$ is strictly increasing.
Finally, $I_x \left({a}\right) \ge a$ by definition of identity mapping.
It follows by Existential Generalisation that:
:$\forall a \in x: \exists b \in x: I_x \left({b}\right) \ge a$
{{qed}}
Theorem: Cofinal Ordinal Relation is Transitive

Let $x$, $y$, and $z$ be ordinals.
Let $\operatorname {cof}$ denote the cofinal relation.
Then:
:$\map {\operatorname {cof} } {x, y} \land \map {\operatorname {cof} } {y, z} \implies \map {\operatorname {cof} } {x, z}$

Proof:
{{tidy|Clarify and structure}}
The conditions for $z$ being cofinal with $x$ shall be verified individually.
Let $\le$ denote the subset relation.
Since $x \le y$ and $y \le z$, it follows that $x \le z$ by Subset Relation is Transitive
Let $f : y \to x$ be the strictly increasing mapping that satisfies:
:$\forall a \in x: \exists b \in y: \map f b \ge a$
Let $g : z \to y$ be the strictly increasing mapping that satisfies:
:$\forall a \in y: \exists b \in z: \map g b \ge a$
By Composite of Strictly Increasing Mappings is Strictly Increasing:
:$f \circ g$ is a strictly increasing mapping.
Moreover, take any $a \in x$.
There is some $b \in y$ such that:
:$\map f b \ge a$
But $b \in y$, so there is some $c \in z$ such that:
:$\map g c \ge b$
{{begin-eqn}}
{{eqn | l = \map f {\map g c}
      | o = \ge
      | r = \map f b
      | c = $f$ is strictly increasing
}}
{{eqn | l = 
      | o = \ge
      | r = a
      | c = Inequality above
}}
{{end-eqn}}
Therefore:
:$\map {f \circ g} c \ge a$ 
for some $c \in z$.
{{qed}}
Theorem: Cofinal to Zero iff Ordinal is Zero

Let $x$ be an ordinal.
Let $\operatorname{cof}$ denote the cofinal relation.
Let $0$ denote the zero ordinal.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\map {\operatorname{cof} } {x, 0}$}}
{{item|(2):|$\map {\operatorname{cof} } {0, x}$}}
{{item|(3):|$x {{=}} 0$}}
{{end-itemize}}

Proof:
=== $(1) \implies (3)$ ===
If $\map {\operatorname{cof} } {x, 0}$, then there is a function $f : x \to 0$.
If $x \ne 0$, then $x$ has an element $a$.
But then, $\map f a \in 0$, which contradicts the definition of the empty set.
Therefore, $x = 0$.
{{qed|lemma}}
Theorem: Condition for Cofinal Nonlimit Ordinals

Let $x$ and $y$ be nonlimit ordinals.
Let $\operatorname{cof}$ denote the cofinal relation.
Let $\le$ denote the subset relation.
{{explain|This statement could be worded a little more carefully. It is, from examining the link, clear that the subset relation and the ordering relation are the same thing, but it grates to see $\le$ being defined as the subset relation. I'm not saying it ''is'' wrong, because it's not wrong, but it ''looks'' uncomfortable.}}
Furthermore, let $x$ and $y$ satisfy the condition:
:$0 < x \le y$
Then:
:$\map {\operatorname{cof}} { y,x }$

Proof:
Both $x$ and $y$ are non-empty, so by the definition of a limit ordinal:
:$x = z^+$ for some $z$.
:$y = w^+$ for some $w$.
:$\bigcup z^+ \le \bigcup w^+$ follows by Set Union Preserves Subsets/General Result.
:$z \le w$ follows by Union of Successor Ordinal.
Define the function $f : x \to y$ as follows:
:$\map f a = \begin{cases}
a &: a \ne z \\
w &: a = z
\end{cases}$
$a < b \le w$, so $f \left({a}\right) = a$.
Take any $a,b \in x$ such that $a < b$.
:$\map f a < \map f b$ shall be proven by cases:
Theorem: Nonlimit Ordinal Cofinal to One

Let $x$ be a nonlimit non-empty ordinal.
Let $\operatorname{cof}$ denote the cofinal relation. 
Let $1$ denote the ordinal one.
Then:
:$\operatorname{cof} \left({x, 1}\right)$

Proof:
Since $1 = 0^+$, $1$ is not a limit ordinal.
Let $\le$ denote the subset relation.
It follows that $0 < 1$ by Ordinal is Less than Successor.
Moreover, $1 \le x$ follows by the fact that $0 < x$ and Successor of Element of Ordinal is Subset.
Thus we have $0 < 1 \le x$ and so by Condition for Cofinal Nonlimit Ordinals:
:$\operatorname{cof} \left({x, 1}\right)$
{{qed}}
Theorem: Cofinal Limit Ordinals

Let $x$ and $y$ be ordinals.
Let $\mathrm {cof}$ denote the cofinal relation.
Let $K_{II}$ denote the class of all limit ordinals.
Then:
:$\map {\mathrm {cof} } {x, y} \implies \paren {x \in K_{II} \iff y \in K_{II} }$

Proof:
=== Necessary Condition ===
Suppose $y \in K_{II}$.
$x \ne 0$ by Cofinal to Zero iff Ordinal is Zero.
If $x = z^+$ for some $z$, then $z = \bigcup x$ by Union of Successor Ordinal.
Therefore, $z$ would be the least upper bound of $x$.
Since $\map {\mathrm {cof} } {x, y}$, it follows by the definition of cofinal that:
:$\forall a \in x: \exists b \in y: \map f b \ge a$
So $\map f b \ge z$ for some $b \in y$.
But since $y$ is a limit ordinal, $b^+ \in y$ by Successor of Ordinal Smaller than Limit Ordinal is also Smaller.
Therefore, $\map f {b^+} \in x$ and $\map f {b^+} > \map f b \ge z$, which contradicts the fact that $z$ is an upper bound of $x$.
Therefore, $x \ne z^+$ for any $z$ and $x \in K_{II}$.
{{qed|lemma}}
Theorem: Smallest Positive Integer Combination is Greatest Common Divisor

Let $a, b \in \Z_{>0}$ be (strictly) positive integers.
Let $d \in \Z_{>0}$ be the smallest positive integer such that:
: $d = a s + b t$
where $s, t \in \Z$.
Then:
:$(1): \quad d \divides a \land d \divides b$
:$(2): \quad c \divides a \land c \divides b \implies c \divides d$
where $\divides$ denotes divisibility.
That is, $d$ is the greatest common divisor of $a$ and $b$.

Proof:
Let $D$ be the subset of $\Z_{>0}$ defined as:
:$D = \set {a s + b t: s, t \in \Z, a s + b t > 0}$
Setting $s = 1$ and $t = 0$ it is clear that $a = \paren {a \times 1 + b \times 0} \in D$.
So $D \ne \O$.
By Set of Integers Bounded Below by Integer has Smallest Element, $D$ has a smallest element $d$, say.
Thus $d = a s + b t$ for some $s, t \in \Z$.
=== Proof of $(1)$ ===
From the Division Theorem we can write $a = q d + r$ for some $q, r$ with $0 \le r < d$.
If $r \ne 0$ we have:
{{begin-eqn}}
{{eqn | l = r
      | r = a - q d
      | c = 
}}
{{eqn | r = a - q \paren {a s + b t}
      | c = 
}}
{{eqn | r = a \paren {1 - q s} + b \paren {-q t}
      | c = 
}}
{{end-eqn}}
So by definition of $D$, it is clear that $r \in D$.
But $r < d$ which contradicts the stipulation that $d$ is the smallest element of $D$.
Thus $r = 0$ and so $a = q d$.
That is $d \divides a$.
By the same argument, it follows that $d \divides b$ also.
{{qed|lemma}}
=== Proof of $(2)$ ===
Let $c \divides a$ and $c \divides b$.
Then:
: $\exists u, v \in \Z: a = c u, b = c v$
Thus:
{{begin-eqn}}
{{eqn | l = d
      | r = a s + b t
      | c = 
}}
{{eqn | r = c u s + c v t
      | c = 
}}
{{eqn | r = c \paren {u s + v t}
      | c = 
}}
{{end-eqn}}
demonstrating that $c \divides d$.
{{qed}}
Theorem: Smallest Positive Integer Combination is Greatest Common Divisor

Let $a, b \in \Z_{>0}$ be (strictly) positive integers.
Let $d \in \Z_{>0}$ be the smallest positive integer such that:
: $d = a s + b t$
where $s, t \in \Z$.
Then:
:$(1): \quad d \divides a \land d \divides b$
:$(2): \quad c \divides a \land c \divides b \implies c \divides d$
where $\divides$ denotes divisibility.
That is, $d$ is the greatest common divisor of $a$ and $b$.

Proof:
From Bézout's Identity we have:
Let $a, b \in \Z$ such that $a$ and $b$ are not both zero.
Let $\gcd \set {a, b}$ be the greatest common divisor of $a$ and $b$.
Then:
:$\exists x, y \in \Z: a x + b y = \gcd \set {a, b}$
Furthermore, $\gcd \set {a, b}$ is the smallest positive integer combination of $a$ and $b$.
In this instance, $a, b \in \Z_{>0}$ and are therefore both non-zero.
The result then follows by definition of greatest common divisor:
$d = \gcd \set {a, b}$ {{iff}}:
:$(1): \quad d \divides a \land d \divides b$
:$(2): \quad c \divides a \land c \divides b \implies c \divides d$
{{qed}}
Theorem: Matrix is Nonsingular iff Determinant has Multiplicative Inverse

Let $R$ be a commutative ring with unity.
Let $\mathbf A \in R^{n \times n}$ be a square matrix of order $n$.
Then $\mathbf A$ is nonsingular {{iff}} its determinant is a invertible in $R$.
If $R$ is one of the standard number fields $\Q$, $\R$ or $\C$, this translates into:
:$\mathbf A$ is nonsingular {{iff}} its determinant is non-zero.

Proof:
=== Necessary Condition ===
{{:Matrix is Nonsingular iff Determinant has Multiplicative Inverse/Necessary Condition}}
Theorem: Definition:Smith-Volterra-Cantor Set

Let $G$ be a Cantor collection.
Let $g_0 \in G$ such that $\map \mu {g_0} = b$.
Let $p$ be a natural number.
Then there are two nonempty disjoint sets $N_p$ and $P$ such that:
:$g_0 = N_p \bigcup P$
where $N_p$ is nowhere dense in the relative topology on $g_0$ and $\map \mu P \le b / p$.

Proof:
Let $n = p + 1$ for $G, g_0, p, b$ as given in the hypothesis.
We construct our Cantor set by removing a diminishing proportion of sets available.
The construction will be accomplished using two techniques.
First, a ``conversational" approach, then one with more mathematical symbolism, or ``rigor".
Theorem: Prime Groups of Same Order are Isomorphic

Two prime groups of the same order are isomorphic to each other.

Proof:
Let $G_1$ and $G_2$ be prime groups, both of finite order $p$.
From Prime Group is Cyclic, both $G_1$ and $G_2$ are cyclic.
The result follows directly from Cyclic Groups of Same Order are Isomorphic.
{{Qed}}
Theorem: Infinite Cyclic Group is Unique up to Isomorphism

All infinite cyclic groups are isomorphic.
That is, up to isomorphism, there is only one infinite cyclic group.

Proof:
Let $G_1$ and $G_2$ be infinite cyclic groups.
From Infinite Cyclic Group is Isomorphic to Integers we have:
:$G_1 \cong \struct {\Z, +} \cong G_2$
where $\struct {\Z, +}$ is the additive group of integers.
From Isomorphism is Equivalence Relation it follows that:
:$G_1 \cong  G_2$
{{Qed}}