avewright/proofwiki-math huggingface dataset:
Theorem: Principle of Recursive Definition for Peano Structure

Let $\struct {P, 0, s}$ be a Peano structure.
Let $T$ be a set.
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: P \to T$ such that:
:<nowiki>$\forall x \in P: \map f x = \begin{cases}
a & : x = 0 \\
\map g {\map f n} & : x = \map s n
\end{cases}$</nowiki>

Proof:
For each $n \in P$, define $\map A n$ as:
:$\map A n = \set {h: P \to T \mid \map h 0 = a \land \forall m < n: \map h {\map s n} = \map g {\map h m} }$
{{MissingLinks|Ordering $<$ on Peano Structure}}
First, we prove for all $n \in P$ that $\map A n$ is not empty.
More formally, we prove that $A = \set {n \in P: \map A n \ne \O} = P$.
For $n = 0$, there are no $m < n$, so any mapping $h: P \to T$ with $\map h 0 = a$ is an element of $\map A 0$.
Since the constant mapping $\map h n = a$ satisfies this condition, it follows that $0 \in A$.
Now suppose that $n \in A$, and let $h \in \map A n$.
Define $h': P \to T$ by, for all $n' \in P$:
:<nowiki>$\map {h'} {n'} = \begin {cases}
\map h {n'} & : n' \le n \\
\map g {\map h n} & : n' > n
\end {cases}$</nowiki>
To check that $h' \in \map A {\map s n}$, we have to verify that:
:$\forall m < \map s n: \map {h'} {\map s m} = \map g {\map {h'} m}$
Since $h \in \map A n$, only the case $m = n$ needs to be verified:
{{begin-eqn}}
{{eqn | l = \map {h'} {\map s n}
      | r = \map g {\map h n}
      | c = as $\map s n > n$
}}
{{eqn | r = \map g {\map {h'} n}
      | c = Definition of $h'$
}}
{{end-eqn}}
Therefore $h' \in \map A {\map s n}$, and so $\map A {\map s n} \ne \O$.
That means $\map s n \in A$, and by Axiom $(\text P 5)$, we conclude $A = P$.
Now let $A' = \set {n \in P: \forall h, h' \in \map A n: \map h n = \map {h'} n}$.
Then by definition of $\map A )$, it follows that $0 \in A'$.
Suppose now that $n \in A'$, and let $h, h' \in \map A {\map s n}$.
Then:
{{begin-eqn}}
{{eqn | l = \map h {\map s n}
      | r = \map g {\map h n}
      | c = as $h \in \map A {\map s n}$
}}
{{eqn | r = \map g {\map {h'} n}
      | c = as $h, h' \in \map A n$
}}
{{eqn | r = \map {h'} {\map s n}
      | c = as $h \in \map A {\map s n}$
}}
{{end-eqn}}
Hence $\map s n \in A'$, and by Axiom $(\text P 5)$, we conclude $A' = P$.
Because any $f: \N \to T$ as in the theorem statement needs to be in all $\map A n$, it follows that such an $f$ is necessarily unique.
Finally, we can define $f: P \to T$ by:
:$\map f n = \map {h_n} n$
where $h_n \in \map A n$.
It is immediate from the definition of the $\map A n$ that:
:$\forall m, n, m < n: \map A n \subseteq \map A m$
Hence, for every $m, n$ such that $m < n$:
:$\map {h_m} m = \map {h_n} m$
Thus, for all $m < n$:
:$\map f m = \map {h_n} m$
Since $h_n \in \map A n$, it follows that also:
:$f \in \map A n$
Thus, since $n$ was arbitrary, it follows that for all $n \in P$:
:$\map f {\map s n} = \map g {\map f n}$
as desired.
{{qed}}
Category:Principle of Recursive Definition
Category:Mapping Theory
Category:Peano's Axioms
mkowvhef8252csdak4cb2nl75ll060n
Theorem: Principle of Recursive Definition for Minimally Inductive Set

Let $\omega$ be the minimally inductive set.
Let $T$ be a set.
Let $a \in T$.
Let $g: T \to T$ be a mapping.
Then there exists exactly one mapping $f: \omega \to T$ such that:
:$\forall x \in \omega: \map f x = \begin {cases}
a & : x = \O \\
\map g {\map f n} & : x = n^+
\end {cases}$
where $n^+$ is the successor set of $n$.

Proof:
{{questionable|The second principle of transfinite recursion that is linked to is not easily applicable to this situation}}
Take the function $F$ generated in Second Principle of Transfinite Recursion.
Set $f = F {\restriction_\omega}$.
{{begin-eqn}}
{{eqn | l = \map f \O
      | r = \map F \O
      | c = $\O \in \omega$
}}
{{eqn | l = \map f {n^+}
      | r = \map F {n^+}
      | c = $n^+ \in \omega$
}}
{{eqn | r = \map g {\map F n}
      | c = Second Principle of Transfinite Recursion
}}
{{eqn | r = \map g {\map f n}
      | c = $n \in \omega$ and the definition of $f$
}}
{{end-eqn}}
Therefore, such a function exists.
Now, suppose there are two functions $f$ and $f'$ that satisfy this:
:$\map f \O = \map {f'} \O$
Then:
{{begin-eqn}}
{{eqn | l = \map f {n^+}
      | r = \map g {\map f n}
      | c = {{hypothesis}}
}}
{{eqn | r = \map g {\map {f'} n}
      | c = Inductive Hypothesis
}}
{{eqn | r = \map {f'} {n^+}
      | c = {{hypothesis}}
}}
{{end-eqn}}
This completes the proof.
{{qed}}
</onlyinclude>
Theorem: Ordering on 1-Based Natural Numbers is Trichotomy

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $<$ be the strict ordering on $\N_{>0}$.
Then exactly one of the following is true:
:$(1): \quad a = b$
:$(2): \quad a > b$
:$(3): \quad a < b$
That is, $<$ is a trichotomy on $\N_{> 0}$.

Proof:
Using the following axioms:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
Axiom $E$ states:
:$\forall a, b \in \N_{>0}$, either:
::$a = b$, in which case $(1)$ holds
::$\exists x \in \N_{> 0}: a = b + x$, in which case, by definition of the ordering defined, $a > b$, in which case $(2)$ holds
::$\exists x \in \N_{> 0}: a + x = b$, in which case, by definition of the ordering defined, $a < b$, in which case $(3)$ holds.
Hence the result.
{{qed}}
Theorem: Quaternion Modulus of Product of Quaternions

Let $\mathbf x, \mathbf y$ be quaternions.
Let $\size {\mathbf x}$ be the modulus of $\mathbf x$.
Then:
:$\size {\mathbf {x y} } = \size {\mathbf x} \size {\mathbf y}$

Proof:
Let $\mathbf x, \mathbf y$ be in their matrix form.
Then:
{{begin-eqn}}
{{eqn | l = \size {\mathbf {x y} }
      | r = \sqrt {\map \det {\mathbf {x y} } }
      | c = {{Defof|Quaternion Modulus}}
}}
{{eqn | r = \sqrt {\map \det {\mathbf x} \map \det {\mathbf y} }
      | c = Determinant of Matrix Product
}}
{{eqn | r = \sqrt {\map \det {\mathbf x} } \sqrt {\map \det {\mathbf y} }
      | c = Exponent Combination Laws
}}
{{eqn | r = \size {\mathbf x} \size {\mathbf y}
      | c = {{Defof|Quaternion Modulus}}
}}
{{end-eqn}}
{{qed}}
Category:Quaternion Modulus
d26nmjzw4bcr11vkrn54qlzizt67q0c
Theorem: Octonion Conjugation is Involution

Let $x = \tuple {a, b}: a, b \in \mathbb H$ be a octonion.
Let $\overline x$ be the conjugate of $x$.
Then:
:$\overline \cdot: x \mapsto \overline x$
is an involution.
That is:
:$\overline {\paren {\overline x} } = x$

Proof:
{{begin-eqn}}
{{eqn | l = \overline {\paren {\overline x} }
      | r = \overline {\paren {\overline {\tuple {a, b} } } }
      | c = {{Defof|Octonion}}
}}
{{eqn | r = \overline {\tuple {\overline a, -b} }
      | c = {{Defof|Conjugate of Octonion}}
}}
{{eqn | r = \tuple {\overline {\paren {\overline a} }, -\paren {-b} }
      | c = {{Defof|Conjugate of Octonion}}
}}
{{eqn | r = \tuple {a, b}
      | c = Quaternion Conjugation is Involution
}}
{{eqn | r = x
      | c = {{Defof|Octonion}}
}}
{{end-eqn}}
{{qed}}
Category:Octonions
Category:Involutions
sr6an7ebrb6i8b07h018s11isrpfhg5
Theorem: Ordering on 1-Based Natural Numbers is Compatible with Addition

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $+$ denote addition on $\N_{>0}$.
Let $<$ be the strict ordering on $\N_{>0}$.
Then:
:$\forall a, b, n \in \N_{>0}: a < b \implies a + n < b + n$
That is, $>$ is compatible with $+$ on $\N_{>0}$.

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = <
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists c \in \N_{>0}
      | l = a
      | r = b + c
      | c = {{Defof|Ordering on 1-Based Natural Numbers|Ordering on $1$-Based Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = a + n
      | r = \paren {b + c} + n
      | c = {{Defof|Binary Operation}}
}}
{{eqn | r = b + \paren {c + n}
      | c = Natural Number Addition is Associative
}}
{{eqn | r = b + \paren {n + c}
      | c = Natural Number Addition is Commutative
}}
{{eqn | r = \paren {b + n} + c
      | c = Natural Number Addition is Associative
}}
{{eqn | ll= \leadsto
      | l = a + n
      | o = < 
      | r = b + n
      | c = {{Defof|Ordering on 1-Based Natural Numbers|Ordering on $1$-Based Natural Numbers}}
}}
{{end-eqn}}
{{qed}}
Theorem: Ordering on 1-Based Natural Numbers is Compatible with Multiplication

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $\times$ denote multiplication on $\N_{>0}$.
Let $<$ be the strict ordering on $\N_{>0}$.
Then:
:$\forall a, b, n \in \N_{>0}: a < b \implies a \times n < b \times n$
That is, $<$ is compatible with $\times$ on $\N_{>0}$.

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = <
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists c \in \N_{>0}
      | l = a
      | r = b + c
      | c = {{Defof|Ordering on 1-Based Natural Numbers|$<$ on $\N_{>0}$}}
}}
{{eqn | ll= \leadsto
      | l = a \times n
      | r = \paren {b + c} \times n
      | c = {{Defof|Binary Operation}}
}}
{{eqn | r = \paren {b \times n} + \paren {c \times n}
      | c = Natural Number Multiplication Distributes over Addition
}}
{{eqn | ll= \leadsto
      | l = a \times n
      | o = < 
      | r = b \times n
      | c = {{Defof|Ordering on 1-Based Natural Numbers|$<$ on $\N_{>0}$}}: $c \times n \in \N_{> 0}$
}}
{{end-eqn}}
{{qed}}
Theorem: Integral between Limits is Independent of Direction

Let $f$ be a real function which is integrable on the interval $\openint a b$.
Then:
:$\ds \int_a^b \map f x \rd x = \int_a^b \map f {a + b - x} \rd x$

Proof:
Let $z = a + b - x$.
Then:
:$\dfrac {\d z} {\d x} = -1$
and:
:$x = a \implies z = a + b - a = b$
:$x = b \implies z = a + b - b = a$
So:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f {a + b - x} \rd x
      | r = \int_b^a \map f z \paren {-1} \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \int_a^b \map f z \rd z
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = \int_a^b \map f x \rd x
      | c = renaming variables
}}
{{end-eqn}}
{{qed}}
Category:Definite Integrals
657vwqwz0lc70jyt38jen81j7fstvhr
Theorem: Countable Set equals Range of Sequence

Let $S$ be a set.
Then $S$ is countable {{iff}} there exists a sequence $\sequence {s_i}_{i \mathop \in N}$ where $N$ is a subset of $\N$ such that $S$ equals the range of $\sequence {s_i}_{i \mathop \in N}$.

Proof:
=== Necessary Condition ===
Assume that $S$ is countable.
We need to prove that there exists a sequence $\sequence {s_i}_{i \mathop \in N}$, $N \subseteq \N$, such that $S$ equals the range of $\sequence {s_i}_{i \mathop \in N}$.
The range of $\sequence {s_i}_{i \mathop \in N}$ is defined as $\set {s_i: i \in N}$.
;Case 1. $S$ is empty.
Empty Set is Countable confirms that $S$ is countable.
Define the empty sequence as $\sequence {s_i}_{i \mathop \in \O}$.
The range of the empty sequence is $\set {s_i: i \in \O} = \O$.
$S$ equals the range of the empty sequence as $S$ equals $\O$.
This finishes the argument for this case.
;Case $2$. $S$ is finite and not empty.
Let $n \in \N_{>0}$ be the number of elements of $S$.
Define a sequence $\sequence {s_i}_{1 \mathop \le \mathop i \mathop \le \mathop n}$ by going through every element of S:
:Let $s_1$ be any element of $S$.
:Let $s_2$ be any element of $S \setminus \set {s_1}$.
:...
:Let $s_n$ be the single element of $S \setminus \set {s_i: 1 \le i \le n - 1}$.
From this definition follows that every element of $S$ equals some $s_i$, $1 \le i \le n$.
So, $S \subseteq \set {s_i: 1 \le i \le n}$.
Every number $s_i$, $1 \le i \le n$, equals some element of $S$.
So, $\set {s_i: 1 \le i \le n} \subseteq S$.
Accordingly, $S = \set {s_i: 1 \le i \le n}$.
By the definition of range, $\set {s_i: 1 \le i \le n}$ equals the range of the sequence $\sequence {s_i}_{1 \mathop \le \mathop i \mathop \le \mathop n}$.
Therefore, $S$ equals the range of $\sequence {s_i}_{1 \mathop \le \mathop i \mathop \le \mathop n}$.
This finishes the proof for case 2.
;Case $3$. $S$ is infinite.
Since $S$ is countable and infinite, $S$ is countably infinite.
By the definition of countably infinite, $S$ can be written:
:$\set {t_0, t_1, \ldots, t_n, \ldots}$
where $n$ runs over all the natural numbers, $\N$.
In other words, we have:
:$S = \set {t_i: i \in \N}$
We intend to produce a sequence from $S$.
We start with the empty sequence.
Using $\N$, the set to which $S$ is equivalent, we put all the elements of $S$ one by one into the sequence.
The result is $\sequence {t_i}_{i \mathop \in \N}$.
The range of $\sequence {t_i}_{i \mathop \in \N}$ is $\set {t_i: i \in \N}$, which equals $S$.
In other words, $S$ is the range of the sequence $\sequence {t_i}_{i \mathop \in \N}$.
This finishes the necessary part of the proof.
{{qed}}
Theorem: Equivalence of Definitions of Connected Set

{{TFAE|def = Connected Set (Topology)|view = Connected Set|context = Topology (Mathematical Branch)|contextview = Topology}}
Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$ be a non-empty subset of $S$.

Proof:
In order to prove equivalence, it is to be shown that if a subset of a topological space is not connected by one of the given definitions above, then it will likewise not be connected by one of the other definitions.
Equivalence of definitions for connected set will then follow by the Rule of Transposition.
Theorem: Initial Segment of Natural Numbers determined by Zero is Empty

Let $\N_k$ denote the initial segment of the natural numbers determined by $k$:
:$\N_k = \set {0, 1, 2, 3, \ldots, k - 1}$
Then $\N_0 = \O$.

Proof:
From the definition of $\N_0$:
:$\N_0 = \set {n \in \N: n < 0}$ 
From the definition of zero, $0$ is the minimal element of $\N$.
So there is no element $n$ of $\N$ such that $n < 0$.
Thus $\N_0 = \O$.
{{qed}}
Category:Natural Numbers
qbigqp7k4plig58dwsn1gh24fsrjyqb
Theorem: Initial Segment of One-Based Natural Numbers determined by Zero is Empty

Let $\N^*_k$ denote the initial segment of the one-based natural numbers determined by $k$:
:$\N^*_k = \set {1, 2, 3, \ldots, k - 1, k}$
Then $\N^*_0 = \O$.

Proof:
From the definition of $\N^*_0$:
:$\N^*_0 = \set {n \in \N_{>0}: n \le 0}$ 
From the definition of one, the minimal element of $\N_{>0}$ is $1$.
From Zero Strictly Precedes One we know that $0 < 1$.
So there is no element $n$ of $\N_{>0}$ such that $n \le 0$.
Thus $\N^*_0 = \O$.
{{qed}}
Theorem: Heine-Borel Theorem/Real Line/Closed and Bounded Interval

Let $\closedint a b$, $a < b$, be a closed and bounded real interval.
Let $S$ be a set of open real sets.
Let $S$ be a cover of $\closedint a b$.
Then there is a finite subset of $S$ that covers $\closedint a b$.

Proof:
Consider the set $T = \set {x \in \closedint a b: \closedint a x \text { is covered by a finite subset of } S}$.
Theorem: Addition on 1-Based Natural Numbers is Cancellable

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $+$ be addition on $\N_{>0}$.
Then:
:$\forall a, b, c \in \N_{>0}: a + c = b + c \implies a = b$
:$\forall a, b, c \in \N_{>0}: a + b = a + c \implies b = c$
That is, $+$ is cancellable on $\N_{>0}$.

Proof:
By Ordering on $1$-Based Natural Numbers is Trichotomy, one and only one of the following holds:
:$a = b$
:$a < b$
:$b < a$
Suppose $a < b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$a + c < b + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a + c = b + c$.
Similarly, suppose $b > a$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$b + c < a + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a + c = b + c$.
The only other possibility is that $a = b$.
So 
:$\forall a, b, c \in \N_{>0}: a + c = b + c \implies a = b$
and so $+$ is right cancellable on $\N_{>0}$.
From Natural Number Addition is Commutative and Right Cancellable Commutative Operation is Left Cancellable:
:$\forall a, b, c \in \N_{>0}: a + b = a + c \implies b = c$
So $+$ is both right cancellable and left cancellable on $\N_{>0}$.
Hence the result.
{{qed}}
Theorem: Addition on 1-Based Natural Numbers is Cancellable for Ordering

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $<$ be the strict ordering on $\N_{>0}$.
Let $+$ be addition on $\N_{>0}$.
Then:
:$\forall a, b, c \in \N_{>0}: a + c < b + c \implies a < b$
:$\forall a, b, c \in \N_{>0}: a + b < a + c \implies b < c$
That is, $+$ is cancellable on $\N_{>0}$ for $<$.

Proof:
By Ordering on $1$-Based Natural Numbers is Trichotomy, one and only one of the following holds:
:$a = b$
:$a < b$
:$b < a$
Let $a + c < b + c$.
Suppose $a = b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$a + c = b + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a + c < b + c$.
Similarly, suppose $b < a$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$b + c < a + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a + c < b + c$.
The only other possibility is that $a < b$.
So 
:$\forall a, b, c \in \N_{>0}: a + c = b + c \implies a < b$
and so $+$ is right cancellable on $\N_{>0}$ for $<$.
Let $a + b < a + c$.
Suppose $b = c$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$a + b = a + c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a + b < a + c$.
Similarly, suppose $c < b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Addition:
:$a + c < a + b$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a + b < a + c$.
The only other possibility is that $b < c$.
So 
:$\forall a, b, c \in \N_{>0}: a + b < a + c \implies b < c$
and so $+$ is left cancellable on $\N_{>0}$ for $<$.
From Natural Number Addition is Commutative and Right Cancellable Commutative Operation is Left Cancellable:
:$\forall a, b, c \in \N_{>0}: a + b = a + c \implies b = c$
So $+$ is both right cancellable and left cancellable on $\N_{>0}$.
Hence the result.
{{qed}}
Theorem: Multiplication on 1-Based Natural Numbers is Cancellable

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $\times$ be multiplication on $\N_{>0}$.
Then:
:$\forall a, b, c \in \N_{>0}: a \times c = b \times c \implies a = b$
:$\forall a, b, c \in \N_{>0}: a \times b = a \times c \implies b = c$
That is, $\times$ is cancellable on $\N_{>0}$.

Proof:
By Ordering on $1$-Based Natural Numbers is Trichotomy, one and only one of the following holds:
:$a = b$
:$a < b$
:$b < a$
Suppose $a < b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Multiplication:
:$a \times c < b \times c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a \times c = b \times c$.
Similarly, suppose $b > a$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Multiplication:
:$b \times c < a \times c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a \times c = b \times c$.
The only other possibility is that $a = b$.
So 
:$\forall a, b, c \in \N_{>0}: a \times c = b \times c \implies a = b$
and so $\times$ is right cancellable on $\N_{>0}$.
From Natural Number Multiplication is Commutative and Right Cancellable Commutative Operation is Left Cancellable:
:$\forall , b, c \in \N_{>0}: a \times b = a \times c \implies b = c$
So $\times$ is both right cancellable and left cancellable on $\N_{>0}$.
Hence the result.
{{qed}}
Theorem: Multiplication on 1-Based Natural Numbers is Cancellable for Ordering

Let $\N_{> 0}$ be the $1$-based natural numbers.
Let $\times$ be multiplication on $\N_{>0}$.
Let $<$ be the strict ordering on $\N_{>0}$.
Then:
:$\forall a, b, c \in \N_{>0}: a \times c < b \times c \implies a < b$
:$\forall a, b, c \in \N_{>0}: a \times b < a \times c \implies b < c$
That is, $\times$ is cancellable on $\N_{>0}$ for $<$.

Proof:
By Ordering on $1$-Based Natural Numbers is Trichotomy, one and only one of the following holds:
:$a = b$
:$a < b$
:$b < a$
Let $a \times c < b \times c$.
Suppose $a = b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Multiplication:
:$a \times c = b \times c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a \times c < b \times c$.
Similarly, suppose $b < a$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Multiplication:
:$b \times c < a \times c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a \times c < b \times c$.
The only other possibility is that $a < b$.
So 
:$\forall a, b, c \in \N_{>0}: a \times c = b \times c \implies a < b$
and so $\times$ is right cancellable on $\N_{>0}$ for $<$.
Let $a \times b < a \times c$.
Suppose $b = c$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Multiplication:
:$a \times b = a \times c$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this contradicts the fact that $a \times b < a \times c$.
Similarly, suppose $c < b$.
Then by Ordering on $1$-Based Natural Numbers is Compatible with Multiplication:
:$a \times c < a \times b$
By Ordering on $1$-Based Natural Numbers is Trichotomy, this also contradicts the fact that $a \times b < a \times c$.
The only other possibility is that $b < c$.
So 
:$\forall a, b, c \in \N_{>0}: a \times b < a \times c \implies b < c$
and so $\times$ is left cancellable on $\N_{>0}$ for $<$.
From Natural Number Multiplication is Commutative and Right Cancellable Commutative Operation is Left Cancellable:
:$\forall a, b, c \in \N_{>0}: a \times b = a \times c \implies b = c$
So $+$ is both right cancellable and left cancellable on $\N_{>0}$.
Hence the result.
{{qed}}
Theorem: Index of Trivial Subgroup is Cardinality of Group

Let $G$ be a group whose identity element is $e$.
Let $\set e$ be the trivial subgroup of $G$.
Then:
:$\index G {\set e} = \order G$
where:
:$\index G {\set e}$ denotes the index of $\set e$ in $G$
:$\order G$ denotes the cardinality of $G$.

Proof:
By definition of cardinality and the trivial subgroup:
:$\order {\set e} = 1$
From Lagrange's Theorem:
:$\index G {\set e} = \dfrac {\order G} {\order {\set e} } = \dfrac {\order G} 1 = \order G$
{{qed}}
Theorem: Index is One iff Subgroup equals Group

Let $G$ be a group whose identity element is $e$.
Let $H$ be a subgroup of $G$.
Then:
:$\index G H = 1 \iff G = H$
where $\index G H$ denotes the index of $H$ in $G$.

Proof:
For finite groups, we can apply Lagrange's Theorem:
:$\index G H = \dfrac {\order G} {\order H}$
But then:
:$\dfrac {\order G} {\order H} = 1 \iff \order G = \order H$
Hence the result.
For the general case (including infinite groups) we need to consider the (left) coset space $G / H$.
Note that we must have $e H = H \in G / H$.
Hence:
:$\index G H = 1 \iff G / H = \set H \iff G = H$
{{qed}}
Theorem: Set Equality is Equivalence Relation

Let $S$ be a set.
Set equality is an equivalence relation on the power set $\powerset S$ of $S$.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Subset Relation is Antisymmetric

The subset relation is '''antisymmetric''':
:$\paren {x \subseteq y} \land \paren {y \subseteq x} \iff x = y$
where $x$ and $y$ are sets.

Proof:
This is a direct statement of the definition of set equality:
:$x = y := \paren {x \subseteq y} \land \paren {y \subseteq x}$
{{qed}}
Theorem: There Exists No Universal Set

There exists no set which is an absolutely universal set.
That is:
:$\map \neg {\exists \, \UU: \forall T: T \in \UU}$
where $T$ is any arbitrary object at all.
That is, a set that contains ''everything'' cannot exist.

Proof:
{{AimForCont}} such a $\UU$ exists.
Using the Axiom of Specification, we can create the set:
:$R = \set {x \in \UU: x \notin x}$
But from Russell's Paradox, this set cannot exist.
Thus:
:$R \notin \UU$
and so $\UU$ cannot contain everything.
{{qed}}
Theorem: There Exists No Universal Set

There exists no set which is an absolutely universal set.
That is:
:$\map \neg {\exists \, \UU: \forall T: T \in \UU}$
where $T$ is any arbitrary object at all.
That is, a set that contains ''everything'' cannot exist.

Proof:
Let $\SS$ be the set of all sets.
Then $\SS$ must be an element of itself:
:$\SS \owns \SS$
Thus we have an infinite descending sequence of membership:
:$\SS \owns \SS \owns \SS \owns \cdots$
But by No Infinitely Descending Membership Chains, no such sequence exists, a contradiction.
{{qed}}