avewright/proofwiki-math huggingface dataset:
Theorem: Naturally Ordered Semigroup Axioms imply Commutativity

Consider the naturally ordered semigroup axioms:
{{:Axiom:Naturally Ordered Semigroup Axioms}}
Axioms $\text {NO} 1$, $\text {NO} 2$ and $\text {NO} 3$ together imply the commutativity of the naturally ordered semigroup $\struct {S, \circ, \preceq}$.

Proof:
From {{NOSAxiom|1}}, $\struct {S, \circ, \preceq}$ has a smallest element.
This is identified as '''zero: $0$'''.
From Zero is Identity in Naturally Ordered Semigroup, $0$ is the identity element of $\struct {S, \circ, \preceq}$,
It may be the case that $S$ is a singleton such that $S = \set 0$ .
Then $\struct {S, \circ}$ degenerates to the trivial group.
From Trivial Group is Abelian, it follows that $\circ$ is commutative.
Let $S^* := S \setminus \set 0$ denote the complement of $\set 0$ in $S$.
From {{NOSAxiom|1}}, $S^*$ also has a smallest element.
This we will call $1$.
It will be shown that $1$ commutes with every element of $S$.
Let $T \subseteq S$ be the set of element of $S$ which commute with $1$.
We have {{apriori}} that $0$ is the identity element of $\struct {S, \circ, \preceq}$.
Hence:
:$1 \circ 0 = 1 = 0 \circ 1$
and it is seen that $0 \in T$.
Now suppose $n \in T$.
That is:
:$1 \circ n = n \circ 1$
We have:
{{begin-eqn}}
{{eqn | l = 1 \circ \paren {n \circ 1}
      | r = \paren {1 \circ n} \circ 1
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \paren {n \circ 1} \circ 1
      | c = {{hypothesis}}
}}
{{end-eqn}}
So
:$n \in T \implies n \circ 1 \in T$.
It follows from Principle of Mathematical Induction for Naturally Ordered Semigroup that:
:$T = S$
That is, all the  element of $S$ commute with $1$.
Hence the result.
{{qed}}
Theorem: Positive Rational Numbers under Addition fulfil Naturally Ordered Semigroup Axioms 2 to 4

The algebraic structure:
:$\struct {\Q_{\ge 0}, +, \le}$
is an ordered semigroup which fulfils the axioms:
:{{NOSAxiom|2}}
:{{NOSAxiom|3}}
:{{NOSAxiom|4}}
but:
:does not fulfil {{NOSAxiom|1}}
:$\struct {\Q_{\ge 0}, +}$is not isomorphic to $\struct {\N, +}$.

Proof:
First we note that from Positive Rational Numbers under Addition form Ordered Semigroup:
:$\struct {\Q_{\ge 0}, +, \le}$ is an ordered semigroup.
Theorem: Subsemigroup of Ordered Semigroup is Ordered

Let $\struct {S, \circ, \preceq}$ be an ordered semigroup.
Let $\struct {T, \circ_T}$ be a subsemigroup of $\struct {S, \circ}$.
Then the ordered structure $\struct {T, \circ_T, \preceq_T}$ is also an ordered semigroup.
In the above:
:$\circ_T$ denotes the operation induced on $T$ by $\circ$
:$\preceq_T$ denotes the restriction of $\preceq$ to $T \times T$.

Proof:
It is necessary to ascertain that $\struct {T, \circ {\restriction_T} }$ fulfils the ordered semigroup axioms:
{{:Axiom:Ordered Semigroup Axioms}}
In this context, we see that $\text {OS} 0$ and $\text {OS} 1$ are fulfilled a fortiori by dint of $\struct {T, \circ {\restriction_T} }$ being a subsemigroup of $\struct {S, \circ}$.
We have that $\struct {S, \circ, \preceq}$ is an ordered semigroup.
From Restriction of Ordering is Ordering, we have that $\preceq_T$ is an ordering.
Hence:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | l = a \preceq b
      | o = \implies
      | r = \paren {a \circ c} \preceq \paren {b \circ c}
      | c = Ordered Semigroup Axiom $\text {OS} 2$ on $\struct {S, \circ, \preceq}$
}}
{{eqn | ll= \leadsto
      | q = \forall a, b \in T
      | l = a \preceq_T b
      | o = \implies
      | r = \paren {a \circ_T c} \preceq_T \paren {b \circ_T c}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | l = a \preceq b
      | o = \implies
      | r = \paren {c \circ a} \preceq \paren {c \circ b}
      | c = Ordered Semigroup Axiom $\text {OS} 2$ on $\struct {S, \circ, \preceq}$
}}
{{eqn | ll= \leadsto
      | q = \forall a, b \in T
      | l = a \preceq_T b
      | o = \implies
      | r = \paren {c \circ_T a} \preceq_T \paren {c \circ_T b}
      | c = 
}}
{{end-eqn}}
Hence $\preceq_T$ fulfils Ordered Semigroup Axiom $\text {OS} 2$ on $\struct {T, \circ_T, \preceq_T}$.
{{qed}}
Theorem: Positive Rational Numbers are Closed under Addition

Let $\Q_{\ge 0}$ denote the set of positive rational numbers:
:$\Q_{\ge 0} := \set {x \in \Q: x \ge 0}$
where $\Q$ denotes the set of rational numbers.
Then the algebraic structure $\struct {\Q_{\ge 0}, +}$ is closed in the sense that:
:$\forall a, b \in \Q_{\ge 0}: a + b \in \Q_{\ge 0}$
where $+$ denotes rational addition.

Proof:
Let $a$ and $b$ be expressed in canonical form:
:$a = \dfrac {p_1} {q_1}, b = \dfrac {p_2} {q_2}$
where $p_1, p_2 \in \Z$ and $q_1, q_2 \in \Z_{>0}$.
As $\forall a, b \in \Q_{\ge 0}$ it follows that:
:$p_1, p_2 \in \Z_{\ge 0}$
By definition of rational addition:
:$\dfrac {p_1} {q_1} + \dfrac {p_2} {q_2} = \dfrac {p_1 q_2 + p_2 q_1} {q_1 q_2}$
From Integers form Ordered Integral Domain, it follows that:
{{begin-eqn}}
{{eqn | l = p_1 q_2
      | o = \ge
      | r = 0
}}
{{eqn | l = p_2 q_1
      | o = \ge
      | r = 0
}}
{{eqn | l = q_1 q_2
      | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = p_1 q_2 + p_2 q_1
      | o = \ge
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \dfrac {p_1 q_2 + p_2 q_1} {q_1 q_2}
      | o = \ge
      | r = 0
}}
{{end-eqn}}
{{qed}}
Category:Rational Addition
Category:Rational Numbers
q3ukvjpuyx0si3r5etpdy0zlex9mge7
Theorem: Positive Rational Numbers under Addition form Ordered Semigroup

Let $\Q_{\ge 0}$ denote the set of positive rational numbers.
The algebraic structure:
:$\struct {\Q_{\ge 0}, +, \le}$
forms an ordered semigroup.

Proof:
It is necessary to ascertain that $\struct {\Q_{\ge 0}, +, \le}$ fulfils the ordered semigroup axioms:
{{:Axiom:Ordered Semigroup Axioms}}
From Rational Numbers form Totally Ordered Field, $\struct {\Q, +, \times, \le}$ is a totally ordered field.
Hence $\struct {\Q, +, \le}$ is an ordered group, and so an ordered semigroup.
From Positive Rational Numbers are Closed under Addition we have that $\text {OS} 0$ holds.
From Restriction of Associative Operation is Associative we have that $\text {OS} 1$ holds.
From Restriction of Ordering is Ordering we have that $\text {OS} 2$ holds.
The result follows.
{{qed}}
Theorem: Positive Rational Numbers under Addition form Ordered Semigroup

Let $\Q_{\ge 0}$ denote the set of positive rational numbers.
The algebraic structure:
:$\struct {\Q_{\ge 0}, +, \le}$
forms an ordered semigroup.

Proof:
From Rational Numbers form Totally Ordered Field, $\struct {\Q, +, \times, \le}$ is a totally ordered field.
Hence $\struct {\Q, +, \le}$ is an ordered group, and so an ordered semigroup.
From Positive Rational Numbers are Closed under Addition we have that $\struct {\Q_{\ge 0}, +}$ is closed.
Hence from Subsemigroup Closure Test, $\struct {\Q_{\ge 0}, +}$ is a subsemigroup of $\struct {\Q, +}$.
From Subsemigroup of Ordered Semigroup is Ordered, $\struct {\Q_{\ge 0}, +, \le}$ is an ordered semigroup.
{{qed}}
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Necessary Condition

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $x$ be a rational number.
Then:
:the canonical expansion of $x$ is eventually periodic.

Proof:
Let $\ldots d_n \ldots d_2 d_1 d_0 . d_{-1} d_{-2} \ldots d_{-m}$ be the canonical expansion of $x$.
It is sufficient to show that the canonical expansion $\ldots d_n \ldots d_2 d_1 d_0$ is eventually periodic.
Let $y$ be the $p$-adic number with canonical expansion:
:$\ldots d_n \ldots d_2 d_1 d_0$
We have:
:$y = x - \ds \sum_{i \mathop = -m}^{-1} d_i p^i$ 
So:
:$y$ is a rational number
By definition of $p$-adic integer:
:$y$ is a $p$-adic integer
Let:
:$y = \dfrac a b : a \in \Z, b \in Z_{> 0}$ are coprime
From Characterization of Rational $p$-adic Integer:
:$p \nmid b$
From Prime not Divisor implies Coprime:
:$b, p$ are coprime
=== Lemma 1 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 1}}{{qed|lemma}}
=== Lemma 2 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 2}}{{qed|lemma}}
For all $n \in \N$, let:
:$A_n = \dfrac a b - \paren {p^{n + 1} \dfrac {r_n} b}$
Then:
:$\dfrac a b = A_n + \paren {p^{n + 1} \dfrac {r_n} b}$
From {{Lemma|Canonical P-adic Expansion of Rational is Eventually Periodic|1}}, for all $n \in \N$:
:$A_n \in \N$
:$0 \le A_n \le p^{n+1} - 1$
=== Lemma 3 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 3}}{{qed|lemma}}
=== Lemma 4 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 4}}{{qed|lemma}}
=== Lemma 5 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 5}}{{qed|lemma}}
It follows that $\ldots d_n \ldots d_2 d_1 d_0$ is eventually periodic.
Theorem: Canonical P-adic Expansion of Rational is Eventually Periodic/Sufficient Condition

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $x \in \Q_p$.
Let the canonical expansion of $x$ be eventually periodic.
Then:
:$x$ be a rational number

Proof:
Let the canonical expansion of $x$ be eventually periodic.
=== Lemma 6 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 6}}{{qed|lemma}}
To show that $x$ is a rational number it is sufficient to show that $y$ is a rational number.
Let:
:$\dots d_{k - 1} \ldots d_1 d_0 d_{k - 1} \ldots d_1 d_0 d_{k - 1} \ldots d_1 d_0$
be the periodic canonical expansion of $y$.
By definition of a canonical expansion:
:$y = d_0 + d_1 p + \cdots + d_{k - 1} p^{k - 1} + d_0 p^k + d_1 p^{k + 1} + \cdots + d_{k - 1} p^{2 k - 1} + d_0 p^{2 k} + \cdots$
Let $a = d_0 + d_1 p + \cdots + d_{k - 1} p^{k - 1}$.
Then:
:$y = a \paren {1 + p^k + p^{2 k} + \cdots}$
=== Lemma 7 ===
{{:Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 7}}{{qed|lemma}}
Then:
:$y = \dfrac a {1 - p^k}$
Hence:
:$y$ is a rational number
It follows that $x$ is a rational number.
Theorem: Positive Rational Numbers under Addition form Commutative Monoid

Let $\Q_{\ge 0}$ denote the set of positive rational numbers.
The algebraic structure:
:$\struct {\Q_{\ge 0}, +}$
forms a commutative monoid.

Proof:
From Rational Numbers form Field, $\struct {\Q, +, \times}$ is a field.
Hence $\struct {\Q, +}$ is an abelian group.
From Positive Rational Numbers are Closed under Addition we have that $\struct {\Q_{\ge 0}, +}$ is closed.
Hence from Subsemigroup Closure Test, $\struct {\Q_{\ge 0}, +}$ is a subsemigroup of $\struct {\Q, +}$.
From Restriction of Commutative Operation is Commutative, $\struct {\Q_{\ge 0}, +}$ is a commutative semigroup.
We have that $0$ is the identity element of $\struct {\Q, +}$.
Hence from Identity of Subsemigroup of Group, $0$ is also the identity element of $\struct {\Q_{\ge 0}, +}$.
So $\struct {\Q_{\ge 0}, +}$ is a commutative monoid.
{{qed}}
Category:Examples of Commutative Monoids
Category:Rational Numbers
qvqv41i3g9qftqrq5hh4xxapd1hcye8
Theorem: Positive Rational Numbers under Addition not Isomorphic to Natural Numbers

The positive rational numbers $\Q_{\ge 0}$ under addition:
:$\struct {\Q_{\ge 0}, +}$
is not isomorphic to the natural numbers under addition:
:$\struct {\N, +}$

Proof:
From:
:Positive Rational Numbers under Addition form Commutative Monoid
:Natural Numbers under Addition form Commutative Monoid
both $\struct {\Q_{\ge 0}, +}$ and $\struct {\N, +}$ form commutative monoids.
{{AimForCont}} there exists an semigroup isomorphism $\phi$ from $\struct {\Q_{\ge 0}, +}$ to $\struct {\N, +}$.
By definition of isomorphism:
:$\phi$ is a homomorphism
:$\phi$ is a bijection.
Let $n \in \N$ be odd.
Let $q \in \Q_{\ge 0}$ such that $\map \phi q = n$.
Such a $q$ exists and is unique by definition of bijection.
But then we have:
{{begin-eqn}}
{{eqn | q = \exists m \in \N
      | l = \map \phi {\dfrac q 2}
      | r = m
      | c = {{Defof|Bijection}}
}}
{{eqn | ll= \leadsto
      | l = \map \phi q
      | r = \map \phi {\dfrac q 2 + \dfrac q 2}
      | c = 
}}
{{eqn | r = \map \phi {\dfrac q 2} + \map \phi {\dfrac q 2}
      | c = {{Defof|Semigroup Homomorphism}}
}}
{{eqn | r = m + m
      | c = 
}}
{{eqn | r = 2 m
      | c = 
}}
{{eqn | r = n
      | c = 
}}
{{end-eqn}}
But this contradicts the assertion that $n$ is odd.
So by Proof by Contradiction there can be no such isomorphism from $\struct {\Q_{\ge 0}, +}$ to $\struct {\N, +}$.
Hence the result.
{{qed}}
Theorem: Natural Numbers without 1 fulfil Naturally Ordered Semigroup Axioms 1, 2 and 4

Let $S \subseteq \N$ be the subset of the natural numbers defined as:
:$S = \N \setminus \set 1 = \set {0, 2, 3, 4, \ldots}$
Then the algebraic structure:
:$\struct {S, +, \le}$
is an ordered semigroup which fulfils the axioms:
:{{NOSAxiom|1}}
:{{NOSAxiom|2}}
:{{NOSAxiom|4}}
but:
:does not fulfil {{NOSAxiom|3}}
:$\struct {S, +}$ is not isomorphic to $\struct {\N, +}$.

Proof:
Recall the axioms:
{{:Axiom:Naturally Ordered Semigroup Axioms}}
Theorem: Singleton fulfils Naturally Ordered Semigroup Axioms 1 to 3

Let $S$ be a singleton:
:$S = \set s$
for an arbitrary object $s$.
Let $+$ be the operation on $S$ defined as:
:$\forall s \in S:  s + s = s$
Let $\le$ be the relation defined on $S$ as:
:$s \le s$
Then the algebraic structure:
:$\struct {S, +, \le}$
is an ordered semigroup which fulfils the axioms:
:{{NOSAxiom|1}}
:{{NOSAxiom|2}}
:{{NOSAxiom|3}}
but:
:does not fulfil {{NOSAxiom|4}}
:$\struct {S, +}$ is not isomorphic to $\struct {\N, +}$.

Proof:
Recall the axioms:
{{:Axiom:Naturally Ordered Semigroup Axioms}}
Theorem: Reflexive Relation on Singleton is Well-Ordering

Let $S = \set s$ be a singleton.
Let $\RR$ be a reflexive relation on $S$.
Then $\RR$ is a well-ordering on $S$.

Proof:
Let $S = \set s$.
By definition of reflexive relation:
:$s \mathrel \RR s$
It trivially holds that:
:$\forall a, b \in S: a \mathrel \RR b \land b \mathrel \RR a \implies a = b$
and so $\RR$ is antisymmetric.
It also trivially holds that:
:$\forall a, b, c \in S: a \mathrel \RR b \land b \mathrel \RR c \implies a \mathrel \RR c$
Thus $\RR$ is an ordering on $S$.
We also have trivially that:
:$\forall a, b \in S: a \mathrel \RR b \lor b \mathrel \RR a$
and so $\RR$ is a total ordering on $S$.
Finally from Finite Totally Ordered Set is Well-Ordered:
:$\struct {S, \RR}$ is a well-ordered set.
Hence the result.
{{qed}}
Category:Singletons
Category:Reflexive Relations
Category:Well-Orderings
3ntk8cx8d9vwyzskz7w1591eseqy83u
Theorem: Power Function with Cancellable Element Preserves Strict Ordering in Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be an ordered semigroup.
Let $x, y \in S$ be such that:
:$(1): \quad x \prec y$
:$(2): \quad$ either $X$ or $y$ (or both) is cancellable for $\circ$.
Let $n \in \N_{>0}$ be a strictly positive integer.
Then:
:$x^n \prec y^n$
where $x^n$ is the $n$th power of $x$.

Proof:
{{WLOG}}, suppose $x$ is cancellable for $\circ$.
The proof proceeds by induction.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$x \prec y \implies x^n \prec y^n$
$\map P 1$ is the case:
:$x \prec y \implies x \prec y$
which is trivially true.
Thus $\map P 1$ is seen to hold.
Theorem: Trivial Group is Abelian

The trivial group is an abelian group.

Proof:
From Trivial Group is Cyclic Group, it is shown that the algebraic structure $\struct {\set e, \circ}$ such that $e \circ e = e$ is a cyclic group.
The result follows from Cyclic Group is Abelian.
{{qed}}
Category:Trivial Group
Category:Abelian Groups
jeq7bjs861u6z3t1pxsjr5053col511
Theorem: Equivalence of Definitions of Dipper Semigroup

Let $m \in \N$ be a natural number.
Let $n \in \N_{>0}$ be a non-zero natural number.
{{TFAE|def = Dipper Semigroup}}
=== Definition 1 ===
{{:Definition:Dipper Semigroup/Definition 1}}
=== Definition 2 ===
{{:Definition:Dipper Semigroup/Definition 2}}

Proof:
We have established in Dipper Semigroup is Commutative Semigroup that $\struct {\N_{< \paren {m + n} }, \oplus_{m, n} }$ is a (commutative) semigroup.
Let $\phi_{m, n}$ be the canonical surjection from $\N$ onto $\map D {m, n}$.
It will be established that the restriction of $\phi_{m, n}$ to $\N_{< \paren {m + n} }$ is an isomorphism from the semigroup $\struct {\N_{< \paren {m + n} }, +_{m, n} }$ onto $\struct {\map D {m, n}, \oplus_{m, n} }$.
From Dipper Relation is Equivalence Relation we have that:
:$\RR_{m, n}$ is an equivalence relation
By definition of canonical surjection:
:$\phi_{m, n}: \N_{< \paren {m + n} } \to \map D {m, n}: \map {\phi_{m, n} } x = \eqclass x {\RR_{m, n} }$
By definition $\phi_{m, n}$ is indeed a surjection.
Then we have:
{{begin-eqn}}
{{eqn | q = \forall x, y \in \N_{< \paren {m + n} }
      | l = \map {\phi_{m, n} } x
      | r = \map {\phi_{m, n} } y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{eqn | lo= \lor
      | l = \size {x - y}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{end-eqn}}
Hence $\phi_{m, n}$ is an injection.
Thus $\phi_{m, n}$ is by definition a bijection.
It remains to show that $\phi_{m, n}$ has the morphism property.
Let $x, y \in \N_{< \paren {m + n} }$ be arbitrary.
We have:
{{begin-eqn}}
{{eqn | q = 
      | l = \map {\phi_{m, n} } {x +_{m, n} y}
      | r = \map {\phi_{m, n} } {x + y - k n}
      | c = Definition of $+_{m, n}$: where $k$ is the largest integer satisfying $m + k n \le a + b$
}}
{{eqn | r = \eqclass {x + y - k n} {\RR_{m, n} }
      | c = 
}}
{{eqn | r = \eqclass {x + y} {\RR_{m, n} }
      | c = 
}}
{{eqn | r = \eqclass x {\RR_{m, n} } \oplus_{m, n} \eqclass y {\RR_{m, n} }
      | c = 
}}
{{eqn | r = \map {\phi_{m, n} } x \oplus_{m, n} \map {\phi_{m, n} } y
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Conditional is not Associative

:$p \implies \paren {q \implies r} \not \vdash \paren {p \implies q} \implies r$

Proof:
<onlyinclude>
We apply the Method of Truth Tables:
:<nowiki>$\begin{array}{|ccccc||ccccc|} \hline
p & \implies & (q & \implies & r) & (p & \implies & q) & \implies & r \\
\hline
\F & \T & \F & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \F & \F & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen by inspection, the truth values under the main connectives do not match for all boolean interpretations.
{{qed}}
Theorem: Dipper Operation is Commutative

Let $m, n \in \Z$ be integers such that $m \ge 0, n > 0$.
Let $\N_{< \paren {m \mathop + n} }$ denote the initial segment of the natural numbers:
:$\N_{< \paren {m \mathop + n} } := \set {0, 1, \ldots, m + n - 1}$
The '''dipper operation''' on $\N_{< \paren {m \mathop + n} }$ is commutative.

Proof:
Recall the definition of the '''dipper operation''' on $\N_{< \paren {m \mathop + n} }$ defined as:
:$\forall a, b \in \Z_{>0}: a +_{m, n} b = \begin{cases} a + b & : a + b < m \\ a + b - k n & : a + b \ge m \end{cases}$
where $k$ is the largest integer satisfying:
:$m + k n \le a + b$
Let $a + b < m$.
Then:
{{begin-eqn}}
{{eqn | l = a +_{m, n} b
      | r = a + b
      | c = Definition of $a +_{m, n} b$
}}
{{eqn | r = b + a
      | c = Natural Number Addition is Commutative
}}
{{eqn | r = b +_{m, n} a
      | c = Definition of $b +_{m, n} a$
}}
{{end-eqn}}
Otherwise $a + b \ge m$.
Then:
{{begin-eqn}}
{{eqn | l = a +_{m, n} b
      | r = a + b - k n
      | c = Definition of $a +_{m, n} b$, for some $k \in \N$
}}
{{eqn | r = b + a - k n
      | c = Natural Number Addition is Commutative, for that same $k \in \N$
}}
{{eqn | r = b +_{m, n} a
      | c = Definition of $b +_{m, n} a$
}}
{{end-eqn}}
So in both cases:
:$a +_{m, n} b = b +_{m, n} a$
and the result follows by definition of commutative operation.
{{qed}}
Theorem: Characteristic of Cayley Table of Left Operation

Let $S$ be a finite set.
Let $\leftarrow$ denote the left operation on $S$.
The Cayley table of the algebraic structure $\struct {S, \leftarrow}$ is characterised by the fact that each row contains just one distinct element.

Proof:
A row of a Cayley table headed by $x$ contains all those elements of the form $x \leftarrow y$.
By definition of the left operation:
:$x \leftarrow y = x$
Hence the result.
{{qed}}
Theorem: Characteristic of Cayley Table of Right Operation

Let $S$ be a finite set.
Let $\rightarrow$ denote the right operation on $S$.
The Cayley table of the algebraic structure $\struct {S, \rightarrow}$ is characterised by the fact that each column contains just one distinct element.

Proof:
A column of a Cayley table headed by $y$ contains all those elements of the form $x \rightarrow y$.
By definition of the right operation:
:$x \rightarrow y = y$
Hence the result.
{{qed}}
Theorem: Left Operation is not Commutative

Let $S$ be a finite set.
Let $\leftarrow$ denote the left operation on $S$.
Then $\leftarrow$ is not commutative on $S$ unless $S$ is a singleton.

Proof:
Let $S$ be a singleton, $S = \set s$, say.
Then:
:$s \leftarrow s = s$
and so $\leftarrow$ is trivially commutative on $S$
Otherwise, $\exists s, t \in S$ such that $s \ne t$.
Then:
:$s \leftarrow t = s$
but:
:$t \leftarrow s = t$
and the result follows by definition of commutative operation.
{{qed}}
Theorem: Right Operation is not Commutative

Let $S$ be a finite set.
Let $\rightarrow$ denote the right operation on $S$.
Then $\rightarrow$ is not commutative on $S$ unless $S$ is a singleton.

Proof:
Let $S$ be a singleton, $S = \set s$, say.
Then:
:$s \rightarrow s = s$
and so $\rightarrow$ is trivially commutative on $S$
Otherwise, $\exists s, t \in S$ such that $s \ne t$.
Then:
:$s \rightarrow t = t$
but:
:$t \rightarrow s = s$
and the result follows by definition of commutative operation.
{{qed}}
Theorem: Induced Metric on Surface of Revolution

Let $\struct {\R^3, d}$ be the Euclidean space.
Let $S_C \subseteq \R^3$ be the surface of revolution.
Let the smooth local parametrization of $C$ be:
:$\map \gamma t = \tuple {\map x t, \map y t}$
Then the induced metric on $S_C$ is:
:$g = \paren {\map {x'} t^2 + \map {y'} t^2} d t^2 + \map y t^2 d \theta^2$

Proof:
By Smooth Local Parametrization of Surface of Revolution, the smooth local parametrization of $S_C$ can be written as:
:$\map X {t, \theta} = \tuple {\map y t \cos \theta, \map y t \sin \theta, \map x t}$
By definition, the induced metric on $S_C$ is:
{{begin-eqn}}
{{eqn | l = g
      | r = X^* \tilde g
}}
{{eqn | r = d \paren {\map y t \map \cos \theta}^2 + d \paren {\map y t \map \sin \theta}^2 + d \paren {\map x t}^2
}}
{{eqn | r = \paren {\map {y'} t \map \cos \theta dt - \map y t \map \sin \theta d\theta}^2 + \paren {\map {y'} t \map \sin \theta dt + \map y t \map \cos \theta d\theta}^2 + \paren {\map {x'} t d t}^2
}}
{{eqn | r = \paren {\map {x'} t^2 + \map {y'} t^2} d t^2 + \map y t^2 d \theta^2
}}
{{end-eqn}}
{{qed}}
{{Proofread|Finish the details}}
Theorem: Primitive of Reciprocal of 1 plus Cosine of x

:$\ds \int \frac {\d x} {1 + \cos x} = \tan \frac x 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = \tan \frac x 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 + \cos x}
      | r = \int \frac {\dfrac {2 \rd u} {1 + u^2} } {1 + \dfrac {1 - u^2} {1 + u^2} }
      | c = Weierstrass Substitution
}}
{{eqn | r = \int \frac {2 \rd u} {1 + u^2 + \paren {1 - u^2} }
      | c = multiplying top and bottom by $1 + u^2$
}}
{{eqn | r = \int \d u
      | c = simplifying
}}
{{eqn | r = u + C
      | c = Primitive of Constant
}}
{{eqn | r = \tan \frac x 2 + C
      | c = substituting for $u$
}}
{{end-eqn}}
{{qed}}