avewright/proofwiki-math huggingface dataset:
Theorem: Conjugacy Classes of Quaternion Group

Let $Q = \Dic 2 = \gen {a, b: a^4 = e, b^2 = a^2, a b a = b}$ be the quaternion group.
The conjugacy classes of $\Dic 2$ are:
:$\set e, \set {a^2}, \set {a, a^3}, \set {b, a^2 b}, \set {a b, a^3 b}$

Proof:
From Center of Quaternion Group, we have:
:$\map Z {\Dic 2} = \set {e, a^2}$
Thus from Conjugacy Class of Element of Center is Singleton, $\set e$ and $\set {a^2}$ are two of those conjugacy classes.
By inspection of the Cayley table:
{{:Quaternion Group/Cayley Table}}
we investigate the remaining $6$ elements in turn, starting with $a$:
{{begin-eqn}}
{{eqn | l = a a a^{-1}
      | o = 
      | rr= = a
      | c = 
}}
{{eqn | l = a^2 a \paren {a^2}^{-1}
      | r = a^2 a a^2 = a^5
      | rr= = a
      | c = 
}}
{{eqn | l = a^3 a \paren {a^3}^{-1}
      | r = a^3 a a = a^5
      | rr= = a
      | c = 
}}
{{eqn | l = b a b^{-1}
      | r = b a \paren {a^2 b} = b a^3 b
      | rr= = a^3
      | c = 
}}
{{eqn | l = \paren {a b} a \paren {a b}^{-1}
      | r = \paren {a b} a \paren {a^3 b} = b a^3 b
      | rr= = a^3
      | c = 
}}
{{eqn | l = \paren {a^2 b} a \paren {a^2 b}^{-1}
      | r = \paren {a^2 b} a b
      | rr= = a^3
      | c = 
}}
{{eqn | l = \paren {a^3 b} a \paren {a^3 b}^{-1}
      | r = \paren {a^3 b} a \paren {a b} = \paren {a^2 b} \paren {a b}
      | rr= = a^3
      | c = 
}}
{{end-eqn}}
So we have a conjugacy class:
:$\set {a, a^3}$
Investigating the remaining $4$ elements in turn, starting with $b$:
{{begin-eqn}}
{{eqn | l = a b a^{-1}
      | r = a b a^3
      | rr= = a^2 b
      | c = 
}}
{{eqn | l = a^2 b \paren {a^2}^{-1}
      | r = a^2 b a^2
      | rr= = b
      | c = 
}}
{{eqn | l = a^3 b \paren {a^3}^{-1}
      | r = a^3 b a
      | rr= = a^2 b
      | c = 
}}
{{eqn | l = b b b^{-1}
      | o = 
      | rr= = b
      | c = 
}}
{{eqn | l = \paren {a b} b \paren {a b}^{-1}
      | r = \paren {a b} b \paren {a^3 b} = \paren {a b} a^3
      | rr= = a^2 b
      | c = 
}}
{{eqn | l = \paren {a^2 b} b \paren {a^2 b}^{-1}
      | r = \paren {a^2 b} b b = \paren {a^2 b} a^2
      | rr= = b
      | c = 
}}
{{eqn | l = \paren {a^3 b} b \paren {a^3 b}^{-1}
      | r = \paren {a^3 b} b \paren {a b} = \paren {a^3 b} a
      | rr= = a^2 b
      | c = 
}}
{{end-eqn}}
So we have a conjugacy class:
:$\set {b, a^2 b}$
Investigating the remaining $2$ elements, starting with $a b$:
{{begin-eqn}}
{{eqn | l = a \paren {a b} a^{-1}
      | r = a \paren {a b} a^3 = a^2 b a^3
      | rr= = a^3 b
      | c = 
}}
{{end-eqn}}
We need go no further: the remaining elements $a b$ and $a^3 b$ are in the same conjugacy class:
:$\set {a b, a^3 b}$
Hence the result.
{{qed}}
Theorem: Conjugacy Action on Subsets is Group Action

Let $\powerset G$ be the set of all subgroups of $G$.
For any $S \in \powerset G$ and for any $g \in G$, the conjugacy action:
:$g * S := g \circ S \circ g^{-1}$
is a group action.

Proof:
By {{Group-axiom|2}}, $e \in G$, thus:
{{begin-eqn}}
{{eqn | l = e * S 
      | r = e \circ S \circ e^{-1}
      | c = Definition of $*$
}}
{{eqn | r = S
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Thus {{GroupActionAxiom|2}} is seen to be fulfilled.
Then:
{{begin-eqn}}
{{eqn | l = \paren {g_1 \circ g_2} * S
      | r = \paren {g_1 \circ g_2} \circ S \circ \paren {g_1 \circ g_2}^{-1}
      | c = Definition of $*$
}}
{{eqn | r = g_1 \circ g_2 \circ S \circ \paren {g_2^{-1}  \circ g_1^{-1} }
      | c = Inverse of Group Product
}}
{{eqn | r = g_1 \circ \paren {g_2 \circ S \circ g_2^{-1} } \circ g_1^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = g_1 * \paren {g_2 \circ S \circ g_2^{-1} }
      | c = Definition of $*$
}}
{{eqn | r = g_1 * \paren {g_2 * S}
      | c = Definition of $*$
}}
{{end-eqn}}
Thus {{GroupActionAxiom|1}} is shown to be fulfilled.
{{Qed}}
Theorem: Normed Vector Space Requires Multiplicative Norm on Division Ring

Let $R$ be a normed division ring with a submultiplicative norm $\norm {\, \cdot \,}_R$.
Let $V$ be a vector space that is not a trivial vector space.
Let $\norm {\, \cdot \,}: V \to \R_{\ge 0}$ be a mapping from $V$ to the positive real numbers satisfying the vector space norm axioms.
Then $\norm {\, \cdot \,}_R$ is a multiplicative norm.
That is:
:$\forall r, s \in R: \norm {r s}_R = \norm r_R \norm s_R$

Proof:
Since $V$ is not a trivial vector space:
:$\exists \mathbf v \in V: \mathbf v \ne 0$
By {{NormAxiomVector|1}}:
:$\norm {\mathbf v} > 0$
Let $r, s \in R$:
{{begin-eqn}}
{{eqn | l = \norm {r s}_R \norm {\mathbf v}
      | r = \norm {\paren {r s} \mathbf v}
      | c = {{NormAxiomVector|2}}
}}
{{eqn | r = \norm {r \paren {s \mathbf v} }
      | c = {{Vector-space-axiom|3}}
}}
{{eqn | r = \norm r_R \norm {s \mathbf v}
      | c = {{NormAxiomVector|2}}
}}
{{eqn | r = \norm r_R \norm s_R \norm {\mathbf v}
      | c = {{NormAxiomVector|2}}
}}
{{end-eqn}}
By dividing both sides of the equation by $\norm {\mathbf v}$ then:
:$\norm {r s}_R = \norm r_R \norm s_R$
The result follows.
{{qed}}
Category:Normed Division Rings
Category:Norm Theory
cuhvz9dm2qqh883e1s8b4hte4btdonv
Theorem: Ring with Multiplicative Norm has No Proper Zero Divisors

Let $\struct {R, +, \circ}$ be a ring.
Let its zero be denoted by $0_R$.
Let $\norm {\,\cdot\,}$ be a multiplicative norm on $R$.
Then $R$ has no proper zero divisors. 
That is:
:$\forall x, y \in R^*: x \circ y \ne 0_R$
where $R^*$ is defined as $R \setminus \set {0_R}$.

Proof:
{{AimForCont}}:
:$\exists x, y \in {R^*} : x \circ y = 0_R$
By positive definiteness:
:$x, y \ne 0_R \iff \norm x, \norm y \ne 0$
Thus:
:$\norm x \norm y \ne 0$
But we also have:
{{begin-eqn}}
{{eqn | l = \norm x \norm y
      | r = \norm {x \circ y}
      | c = Multiplicativity
}}
{{eqn | r = \norm {0_R}
      | c = {{hypothesis}}
}}
{{eqn | r = 0
      | c = Positive Definiteness
}}
{{end-eqn}}
a contradiction.
{{qed}}
Category:Norm Theory
Category:Zero Divisors
gyga65l428w4mwggf0xz38xdfmv0t37
Theorem: Finite Ring with Multiplicative Norm is Field

Let $R$ be a finite ring with a multiplicative norm.
Then $R$ is a field.

Proof:
From Ring with Multiplicative Norm has No Proper Zero Divisors, $R$ has no proper zero divisors.
From Finite Ring with No Proper Zero Divisors is Field, $R$ is a field.
{{qed}}
Category:Ring Theory
Category:Field Theory
Category:Norm Theory
enxnwlyyj6tvyk47644xl7ho37i4chw
Theorem: Composition of Distance-Preserving Mappings is Distance-Preserving

Let:
:$\struct {X_1, d_1}$
:$\struct {X_2, d_2}$
:$\struct {X_3, d_3}$
be metric spaces.
Let:
:$\phi: \struct {X_1, d_1} \to \struct {X_2, d_2}$
:$\psi: \struct {X_2, d_2} \to \struct {X_3, d_3}$
be distance-preserving mappings.
Then the composite of $\phi$ and $\psi$ is also a distance-preserving mapping.

Proof:
Let $x,y \in X_1$.
Then:
{{begin-eqn}}
{{eqn | l = \map {d_1} {x,y}
      | r = \map {d_2} {\map \phi x, \map \phi y}
      | c = $\phi$ is a distance-preserving mapping
}}
{{eqn | r = \map {d_3} {\map \psi {\map \phi x}, \map \psi {\map \phi y} }
      | c = $\psi$ is a distance-preserving mapping
}}
{{eqn | r = \map {d_3} {\map {\psi \circ \phi} x, \map {\psi \circ \phi} y}
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
By definition of a distance-preserving mapping, $\psi \circ \phi$ is distance-preserving.
{{qed}}
Category:Metric Spaces
12w5o3bfajkzro7uds7vssu452xnnh8
Theorem: Composition of Isometries is Isometry

Let:
:$\struct {X_1, d_1}$
:$\struct {X_2, d_2}$
:$\struct {X_3, d_3}$
be metric spaces.
Let:
:$\phi: \struct {X_1, d_1} \to \struct {X_2, d_2}$
:$\psi: \struct {X_2, d_2} \to \struct {X_3, d_3}$
be isometries.
Then the composite of $\phi$ and $\psi$ is also an isometry.

Proof:
An isometry is a distance-preserving mapping which is also a bijection.
From Composition of Distance-Preserving Mappings is Distance-Preserving, $\psi \circ \phi$ is a distance-preserving mapping.
From Composite of Bijections is Bijection, $\psi \circ \phi$ is a bijection.
{{qed}}
Category:Metric Spaces
m8cjqegtg9dd5z42hpcuok44xqc5ih0
Theorem: Subgroup Action is Group Action

Let $\struct {G, \circ}$ be a group.
Let $\struct {H, \circ}$ be a subgroup of $G$.
Let $*: H \times G \to G$ be the subgroup action defined for all $h \in H, g \in G$ as:
:$\forall h \in H, g \in G: h * g := h \circ g$
Then $*$ is a group action.

Proof:
Let $g \in G$.
First we note that since $G$ is closed, and $h \circ g \in G$, it follows that $h * g \in G$.
Next we note:
:$e * g = e \circ g = g$
and so {{GroupActionAxiom|2}} is satisfied.
Now let $h_1, h_2 \in G$.
We have:
{{begin-eqn}}
{{eqn | l = \paren {h_1 \circ h_2} * g
      | r = \paren {h_1 \circ h_2} \circ g
      | c = Definition of $*$
}}
{{eqn | r = h_1 \circ \paren {h_2 \circ g}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = h_1 * \paren {h_2 * g}
      | c = Definition of $*$
}}
{{end-eqn}}
and so {{GroupActionAxiom|1}} is satisfied.
Hence the result.
{{qed}}
Theorem: Orbit of Subgroup Action is Coset

Let $\struct {G, \circ}$ be a group.
Let $\struct {H, \circ}$ be a subgroup of $G$.
Let $*: H \times G \to G$ be the subgroup action defined for all $h \in H, g \in G$ as:
:$\forall h \in H, g \in G: h * g := h \circ g$
The orbit of $x \in G$ is the right coset by $x$ of $H$:
:$\Orb x = H x$

Proof:
From Subgroup Action is Group Action we have that $*$ is a group action.
Let $x \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \Orb x
      | r = \set {g \in G: \exists h \in H: g = h * x}
      | c = {{Defof|Orbit (Group Theory)|Orbit}}
}}
{{eqn | r = \set {g \in G: \exists h \in H: g = h \circ x}
      | c = Definition of $*$
}}
{{eqn | r = H x
      | c = 
}}
{{end-eqn}}
Hence the result, by definition of right coset.
{{qed}}
Theorem: Removable Singularity at Infinity implies Constant Function

Let $f : \C \to \C$ be an entire function.
Let $f$ have an removable singularity at $\infty$. 
Then $f$ is constant.

Proof:
We are given that $f$ has a removable singularity at $\infty$.
By Riemann Removable Singularities Theorem, $f$ must be bounded in a neighborhood of $\infty$.
That is, there exists a real number $M > 0$ such that:
:$\forall z \in \set {z : \cmod z > r}: \cmod {\map f z} \le M$
for some real $r \ge 0$.
However, by Continuous Function on Compact Space is Bounded, $f$ is also bounded on $\set {z: \cmod z \le r}$. 
As $\set {z: \cmod z > r} \cup \set {z: \cmod z \le r} = \C$, $f$ is therefore bounded on $\C$.
Therefore by Liouville's Theorem, $f$ is constant.
{{qed}}
Category:Removable Singularities
Category:Entire Functions
Category:Constant Mappings
kqrac3y1dtagcm4gult9smdrrvzmjte
Theorem: Stabilizer of Subgroup Action is Identity

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $\struct {H, \circ}$ be a subgroup of $G$.
Let $*: H \times G \to G$ be the subgroup action defined for all $h \in H, g \in G$ as:
:$\forall h \in H, g \in G: h * g := h \circ g$
The stabilizer of $x \in G$ is $\set e$:
:$\Stab x = \set e$

Proof:
From Subgroup Action is Group Action we have that $*$ is a group action.
Let $x \in G$.
Then:
{{begin-eqn}}
{{eqn | l = \Stab x
      | r = \set {h \in H: h * x = x}
      | c = {{Defof|Stabilizer}}
}}
{{eqn | r = \set {h \in H: h \circ x = x}
      | c = Definition of $*$
}}
{{eqn | r = \set {h \in H: h = x \circ x^{-1} }
      | c = 
}}
{{eqn | r = \set {h \in H: h = e}
      | c = 
}}
{{eqn | r = \set e
      | c = 
}}
{{end-eqn}}
Hence the result, by definition of right coset.
{{qed}}
Theorem: Stabilizers of Elements in Same Orbit are Conjugate Subgroups

Let $G$ be a group acting on a set $X$.
Let:
:$y, z \in \Orb x$
where $\Orb x$ denotes the orbit of some $x \in X$.
Then their stabilizers $\Stab y$ and $\Stab z$ are conjugate subgroups.

Proof:
From Stabilizer is Subgroup we have that both $\Stab y$ and $\Stab z$ are subgroups of $G$.
From definition of orbits:
:$\exists h_1, h_2 \in G: y = h_1 * x, z = h_2 * x$
Then $y = h_1 * \paren {h_2^{-1} * z} = h_1 h_2^{-1} * z$.
Thus:
{{begin-eqn}}
{{eqn | l = \Stab y
      | r = \set {g \in G: g * y = y}
      | c = {{Defof|Stabilizer}}
}}
{{eqn | r = \set {g \in G: g * \paren {h_1 h_2^{-1} * z} = h_1 h_2^{-1} * z}
}}
{{eqn | r = \set {g \in G: h_1^{-1} h_2 * \paren {g h_1 h_2^{-1} * z} = z}
}}
{{eqn | r = \set {g \in G: \paren {h_1 h_2^{-1} }^{-1} g \paren {h_1 h_2^{-1} } * z = z}
}}
{{eqn | r = \paren {h_1 h_2^{-1} } \set {\paren {h_1 h_2^{-1} }^{-1} g \paren {h_1 h_2^{-1} } \in G: \paren {h_1 h_2^{-1} }^{-1} g \paren {h_1 h_2^{-1} } * z = z} \paren {h_1 h_2^{-1} }^{-1}
}}
{{eqn | r = \paren {h_1 h_2^{-1} } \Stab z \paren {h_1 h_2^{-1} }^{-1}
      | c = {{Defof|Stabilizer}}
}}
{{end-eqn}}
This shows that $\Stab y$ and $\Stab z$ are conjugate.
Hence the result.
{{qed}}
Theorem: Stabilizer of Subgroup Action on Left Coset Space

Let $G$ be a group.
Let $H$ and $K$ be subgroups of $G$.
Let $K$ act on the left coset space $G / H^l$ by:
:$\forall \tuple {k, g H} \in K \times G / H^l: k * \paren {g H} := \paren {k g} H$
The stabilizer of $g H$ is $K \cap H^g$, where $H^g$ denotes the $G$-conjugate of $H$ by $g$.

Proof:
{{Proofread| Check the proof for the well-definedness of the action}}
Let $\RR^l_H$ be the equivalence defined as left congruence modulo $H$.
By Left Congruence Class Modulo Subgroup is Left Coset, $\RR^l_H$ is an equivalence relation. 
We check that $*$ is a well-defined mapping over $\RR^l_H$.
Suppose:
:$\eqclass g {\RR^l_H} = \eqclass {g'} {\RR^l_H} $
for some $g, g' \in G$, where $\eqclass g {\RR^l_H}$ and $\eqclass {g'} {\RR^l_H}$ are the equivalence classes of $g \in G$ and $g' \in G$ respectively.
{{improve|This is neither a "let" nor a "suppose", it's a result which needs to be linked from}}
From Left Congruence Class Modulo Subgroup is Left Coset:
:$\eqclass g {\RR^l_H} = g H$
And:
:$\eqclass {g'} {\RR^l_H} = g' H$
Then:
:$\forall g, g' \in G: \paren {g H} = \paren {g' H}$
We have:
{{begin-eqn}}
{{eqn | q = \forall \tuple {k, g H} \in K \times G / H^l
      | l = \paren {k g'} H
      | r = k * \paren {g' H}
      | c = Definition of $*$
}}
{{eqn | r = k * \paren {g H}
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {k g} H
      | c = Definition of $*$
}}
{{end-eqn}}
Thus $*$ is a well-defined mapping over $\RR^l_H$.
Hence:
{{begin-eqn}}
{{eqn | l = \Stab {g H}
      | r = \set {k \in K: \paren {k g} H = g H}
      | c = {{Defof|Stabilizer}}
}}
{{eqn | r = \set {k \in K: g^{-1} \paren {k g} \in H}
      | c = Left Cosets are Equal iff Product with Inverse in Subgroup
}}
{{eqn | r = \set {k \in K: k \in g H g^{-1} }
      | c = Conjugate of Set by Group Product
}}
{{eqn | r = K \cap H^g
      | c = {{Defof|Conjugate of Group Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Length of Orbit of Subgroup Action on Left Coset Space

Let $G$ be a group.
Let $H$ and $K$ be subgroups of $G$.
Let $K$ act on the left coset space $G / H^l$ by:
:$\forall \tuple {k, g H} \in K \times G / H^l: k * g H := \paren {k g} H$
The length of the orbit of $g H$ is $\index K {K \cap H^g}$.

Proof:
{{begin-eqn}}
{{eqn | l = \card {\Orb {g H} }
      | r = \index K {\Stab {g H} }
      | c = Orbit-Stabilizer Theorem
}}
{{eqn | r = \index K {K \cap H^g}
      | c = Stabilizer of Subgroup Action on Left Coset Space
}}
{{end-eqn}}
{{qed}}
Theorem: Pole at Infinity implies Polynomial Function

Let $f : \C \to \C$ be an entire function.
Let $f$ have a pole of order $N$ at $\infty$. 
Then $f$ is a polynomial of degree $N$.

Proof:
By Complex Function is Entire iff it has Everywhere Convergent Power Series, there exists a power series: 
:$\ds \map f z = \sum_{n \mathop = 0}^\infty a_n z^n$ 
convergent for all $z \in \C$, where $\sequence {a_n}$ is a sequence of complex coefficients. 
This gives: 
:$\ds \map f {\frac 1 z} = \sum_{n \mathop = 0}^\infty \frac {a_n} {z^n}$ 
It is given that $\map f z$ has a pole of order $N$ at $\infty$, so $\map f {\dfrac 1 z}$ has a pole of order $N$ at $0$. 
So $N$ is the least positive integer such that:
:$\ds z^N \map f {\frac 1 z} = \sum_{n \mathop = 0}^\infty a_n z^{N - n}$ 
is holomorphic at $0$, with $a_N \ne 0$. 
Therefore, all exponents of $z$, with non-zero coefficients, in this series must be non-negative. 
So $a_n = 0$ for $n > N$.  
Hence: 
:$\ds \map f z = \sum_{n \mathop = 0}^N a_n z^n$
with $a_N \ne 0$. 
That is, $f$ is a polynomial of degree $N$.  
{{qed}}
Category:Complex Analysis
nsozmiozntadk2y7586fa5basx77t9f
Theorem: Cardinality of Set Difference with Subset

Let $S$ and $T$ be sets such that $T$ is finite.
Let $T \subseteq S$.
Then:
:$\card {S \setminus T} = \card S - \card T$
where $\card S$ denotes the cardinality of $S$.

Proof:
From Set Difference with Superset is Empty Set:
:$T \subseteq S \iff T \setminus S = \O$
From Set Difference and Intersection form Partition:
:$S = \paren {S \setminus T} \cup T$
Thus from Cardinality of Set Union:
:$\card S = \card T + \card {S \setminus T} - \card {T \cap \paren {S \setminus T} }$
But from Set Difference Intersection with Second Set is Empty Set:
:$T \cap \paren {S \setminus T} = 0$
Hence the result.
{{qed}}
Theorem: Riemann Zeta Function at Non-Positive Integers

Let $n \ge 0$ be a integer. 
Then: 
:$\map \zeta {-n} = \paren {-1}^n \dfrac {B_{n + 1} } {n + 1}$ 
where:
:$B_n$ is the $n$th Bernoulli number
:$\zeta$ is the Riemann Zeta function

Proof:
By Hankel Representation of Riemann Zeta Function: 
:$\ds \map \zeta {-n} = \frac {i \map \Gamma {1 + n} } {2 \pi} \oint_C \frac 1 {z^{n + 1} \paren {e^z - 1} } \rd z$ 
where $C$ is the Hankel contour.
Note that the integrand is meromorphic, with exactly one pole at $z = 0$ lying inside the contour.
So: 
{{begin-eqn}}
{{eqn | l = \map \zeta {-n}
      | r = \frac {i n!} {2 \pi} \oint_C \frac 1 {\paren {-z}^{n + 2} } \cdot \frac {-z} {e^z - 1} \rd z
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = -\frac {i n!} {2 \pi} \cdot 2 \pi i \, \Res {\frac 1 {\paren {-z}^{n + 2} } \cdot \frac {-z} {e^z - 1} } 0
      | c = Cauchy's Residue Theorem 
}}
{{eqn | r = n! \, \Res {\paren {-1}^2 \paren {-1}^n \sum _{k \mathop = 0}^\infty \frac {B_k} {k!} z^{k - n - 2} } 0
      | c = {{Defof|Bernoulli Numbers|subdef = Generating Function}}, $i^2 = -1$
}}
{{eqn | r = n! \paren {-1}^n \, \Res {\sum_{k \mathop = 0}^\infty \frac {B_k} {k!} z^{k - n - 2} } 0
}}
{{end-eqn}}
By the definition of a residue, the residue at $0$ is given by the coefficient of the $\dfrac 1 z$ term.
This is the term where $k = n + 1$, so:
{{begin-eqn}}
{{eqn | l = \map \zeta {-n}
      | r = n! \paren {-1}^n \frac {B_{n + 1} } {\paren {n + 1}!} 
}}
{{eqn | r = \paren {-1}^n \frac {B_{n + 1} } {n + 1}
}}
{{end-eqn}}
{{qed}}
Theorem: Remainder on Division is Least Positive Residue

Let $a, b \in \Z$ be integers such that $a \ge 0$ and $b \ne 0$.
Let $r$ be the remainder resulting from the operation of integer division of $a$ by $b$:
$a = q b + r, 0 \le r < \size b$
Then $r$ is equal to the least positive residue of $a \pmod b$.

Proof:
By definition of least positive residue:
:$a = q b + r \iff r \equiv a \pmod b$
for some $q \in \Z$.
By the Division Theorem, there exists a $q$ such that:
:$0 \le r < \size b$
which is precisely the definition of the least positive residue of $a \pmod b$.
{{qed}}
Theorem: Floor Function/Examples/Floor of Root 5

:$\floor {\sqrt 5} = 2$

Proof:
The decimal expansion of $\sqrt 5$ is:
:$\sqrt 5 \approx 2 \cdotp 23606 \, 79774 \, 99789 \, 6964 \ldots$
Thus:
:$2 \le \sqrt 5 < 3$
Hence $2$ is the floor of $\sqrt 5$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of 3

:$\floor 3 = 3$

Proof:
We have that $3$ is an integer.
Thus this is a specific example of Real Number is Integer iff equals Floor:
$\floor x = x \iff x \in \Z$
{{qed}}
Theorem: Divisibility by 12

Let $N \in \N$ be expressed as:
:$N = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n$
Then $N$ is divisible by $12$ {{iff}} $a_0 - 2 a_1 + 4 \paren {\ds \sum_{r \mathop = 2}^n a_r}$ is  divisible by $12$.

Proof:
We first prove that $100 \times 10^n = 4 \pmod {12}$, where $n \in \N$.
Proof by induction:
For all $n \in \N$, let $P \paren n$ be the proposition:
:$100 \times 10^n = 4 \pmod {12}$
Theorem: Exponential on Real Numbers is Injection

Let $\exp: \R \to \R$ be the exponential function:
:$\map \exp x = e^x$
Then $\exp$ is an injection.

Proof:
<onlyinclude>
From Exponential is Strictly Increasing:
:$\exp$ is strictly increasing on $\R$.
From Strictly Monotone Mapping with Totally Ordered Domain is Injective:
:$\exp$ is an injection.
{{qed}}
Theorem: Surjective Restriction of Real Exponential Function

Let $\exp: \R \to \R$ be the exponential function:
:$\map \exp x = e^x$
Then the restriction of the codomain of $\exp$ to the strictly positive real numbers:
:$\exp: \R \to \R_{>0}$
is a surjective restriction.
Hence:
:$\exp: \R \to \R_{>0}$
is a bijection.

Proof:
We have Exponential on Real Numbers is Injection.
Let $y \in \R_{> 0}$.
Then $\exists x \in \R: x = \map \ln y$
That is:
:$\exp x = y$
and so $\exp: \R \to \R_{>0}$ is a surjection.
Hence the result.
{{qed}}
Theorem: Maximum Rule for Real Sequences

:$\ds \lim_{n \mathop \to \infty} \max \set {x_n, y_n} = \max \set {l, m}$

Proof:
=== Case $1$: $l = m$ ===
Let $l = m$.
Then:
:$\max \set {l, m} = l = m$
Let $\epsilon > 0$ be given.
By definition of the limit of a real sequence, we can find $N_1$ such that:
:$\forall n > N_1: \size {x_n - l} < \epsilon$
Similarly we can find $N_2$ such that:
:$\forall n > N_2: \size {y_n - m} < \epsilon$
Let $N = \max \set {N_1, N_2}$.
Then if $n > N$, both the above inequalities will be true:
:$n > N_1$
:$n > N_2$
Thus $\forall n > N$:
:if $y_n < x_n$ then:
::$\size {\max \set {x_n, y_n} - \max \set {l, m} } = \size {x_n - l} < \epsilon$
:if $x_n \le y_n$ then:
::$\size {\max \set {x_n, y_n} - \max \set {l, m} } = \size {y_n - m} < \epsilon$
In either case:
: $\size {\max \set {x_n, y_n} - \max \set {l, m} } < \epsilon$
The result follows.
{{qed|lemma}}
Theorem: Minimum Rule for Real Sequences

:$\ds \lim_{n \mathop \to \infty} \min \set {x_n, y_n} = \min \set {l, m}$

Proof:
By Sum Less Maximum is Minimum:
:$\forall n \in \R: \min \set {x_n, y_n} = x_n + y_n - \max \set {x_n, y_n}$
and
:$\min \set {m, l} = m + l - \max \set {m, l}$
By Maximum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \max \set {x_n, y_n} = \max \set {m, l}$
By the Multiple Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} - \max \set {x_n, y_n} = - \max \set {m, l}$
By the Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty}  x_n + y_n - \max \set {x_n, y_n} = m + l - \max \set {m, l}$
Hence:
:$\ds \lim_{n \mathop \to \infty} \min \set {x_n, y_n} = \min \set {l, m}$
{{qed}}
Theorem: Division Subring of Normed Division Ring

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $S$ be a division subring of $R$.
Then:
:$\struct {S, \norm {\, \cdot \,}_S}$ is a normed division subring of $\struct {R, \norm {\, \cdot \,} }$
where $\norm {\, \cdot \,}_S$ is the norm $\norm {\,\cdot\,}$ restricted to $S$.

Proof:
=== {{Norm-axiom-mult|1|nolink}} ===
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \norm x_S
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \norm x
      | r = 0
      | c = Definition of $\norm x_S$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = 0
      | c = {{Norm-axiom-mult|1}}
}}
{{end-eqn}}
{{qed|lemma}}