avewright/proofwiki-math huggingface dataset:
Theorem: Modulus 1 Rational Argument Complex Numbers under Multiplication form Infinite Abelian Group

Let $S$ be the set defined as:
:$S = \set {\cos \theta + i \sin \theta: \theta \in \Q}$
Then the algebraic structure $\struct {S, \times}$ is an infinite abelian group.

Proof:
By definition of polar form of complex numbers, the elements of $S$ are also elements of the circle group $\struct {K, \times}$:
:$K = \set {z \in \C: \cmod z = 1}$
$S$ is infinite by construction.
Thus $S \subseteq C$ and trivially $S \ne \O$.
Let $a, b \in S$.
Then:
:$a = \cos \theta_1 + i \sin \theta_1$
and:
:$b = \cos \theta_2 + i \sin \theta_2$
for some $\theta_1, \theta_2 \in \Q$.
We have that:
{{begin-eqn}}
{{eqn | l = a \times b
      | r = \paren {\cos \theta_1 + i \sin \theta_1} \paren {\cos \theta_2 + i \sin \theta_2}
      | c = 
}}
{{eqn | r = \map \cos {\theta_1 + \theta_2} + i \map \sin {\theta_1 + \theta_2}
      | c = 
}}
{{eqn | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = b^{-1}
      | r = \cos \theta_2 - i \sin \theta_2
      | c = 
}}
{{eqn | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
Hence by the Two-Step Subgroup Test, $\struct {S, \times}$ is a subgroup of $\struct {K, \times}$.
It has been established that $S$ is an infinite set.
Hence by definition $\struct {S, \times}$ is an infinite group.
Finally, from Subgroup of Abelian Group is Abelian, $\struct {S, \times}$ is an abelian group.
{{qed}}
Theorem: Inversion Mapping is Automorphism iff Group is Abelian

Let $\struct {G, \circ}$ be a group.
Let $\iota: G \to G$ be the inversion mapping on $G$, defined as:
:$\forall g \in G: \map \iota g = g^{-1}$
Then $\iota$ is an automorphism {{iff}} $G$ is abelian.

Proof:
From Inversion Mapping is Permutation, $\iota$ is a permutation.
It remains to be shown that $\iota$ has the morphism property {{iff}} $G$ is abelian.
Theorem: Even Order Group has Odd Number of Order 2 Elements

Let $G$ be a group whose identity is $e$.
Let $G$ be of even order.
Then $G$ has an odd number of elements of order $2$.

Proof:
Let $S = \set {x \in G: \order x > 2}$ be the set of all elements of $G$ whose order is strictly greater than $2$.
Let $h \in S$.
Then from Order of Group Element equals Order of Inverse:
:$h^{-1} \in S$.
Because $\order h > 2$ it follows that $h^{-1} \ne h$ by definition of self-inverse.
Thus every element in $S$ can be paired off with its inverse which is also in $S$.
It follows that $S$ has an even number of elements.
Thus $G \setminus S$ also contains an even number of elements.
From Identity is Only Group Element of Order 1, there is precisely $1$ element of $G$ whose order is less than $2$.
This leaves $G$ with an odd number of elements of order $2$.
{{qed}}
Theorem: Roots of Complex Number/Examples/Cube Roots

Let $z := \polar {r, \theta}$ be a complex number expressed in polar form, such that $z \ne 0$.
Then the complex cube roots of $z$ are given by:
:$z^{1 / 3} = \set {r^{1 / 3} \paren {\map \cos {\dfrac {\theta + 2 \pi k} 3} + i \, \map \sin {\dfrac {\theta + 2 \pi k} 3} }: k \in \set {0, 1, 2} }$
There are $3$ distinct such complex cube roots.
These can also be expressed as:
:$z^{1 / 3} = \set {r^{1 / 3} e^{i \paren {\theta + 2 \pi k} / 3}: k \in \set {0, 1, 2} }$
or:
:$z^{1 / 3} = \set {r^{1 / 3} e^{i \theta / 3} \omega^k: k \in \set {0, 1, 2} }$
where $\omega = e^{2 i \pi / 3} = -\dfrac 1 2 + \dfrac {i \sqrt 3} 2$ is the first cube root of unity.

Proof:
An example of Roots of Complex Number.
{{qed}}
Theorem: Roots of Complex Number/Corollary

Let $z := \polar {r, \theta}$ be a complex number expressed in polar form, such that $z \ne 0$.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $w$ be one of the complex $n$th roots of $z$.
Then the $n$th roots of $z$ are given by:
:$z^{1 / n} = \set {w \epsilon^k: k \in \set {1, 2, \ldots, n - 1} }$
where $\epsilon$ is a primitive $n$th root of unity.

Proof:
By definition of primitive complex $n$th root of unity:
:$\omega = e^{2 m i \pi k}$
for some $m \in \Z: 1 \le m < n$.
Thus:
{{begin-eqn}}
{{eqn | l = \paren {w \omega^k}^n
      | r = w^n \paren {e^{2 m i \pi k / n} }^n
      | c = 
}}
{{eqn | r = z e^{2 m i \pi k}
      | c = 
}}
{{eqn | r = z \paren {e^{2 i \pi} }^{m k}
      | c = 
}}
{{eqn | r = z \times 1^{m k}
      | c = 
}}
{{eqn | r = z
      | c = 
}}
{{end-eqn}}
This demonstrates that $w \omega^k$ is one of the complex $n$th roots of $z$.
All of the complex $n$th roots of unity are represented by powers of $\omega$.
Thus it follows from Roots of Complex Number that:
:$z^{1 / n} = \set {w \omega^k: k \in \set {1, 2, \ldots, n - 1} }$
are the $n$ complex $n$th roots of $z$.
{{qed}}
Theorem: Top is Prime Element

Let $L = \struct {S, \wedge, \preceq}$ be a bounded above meet semilattice.
Then:
:$\top$ is a prime element
where $\top$ denotes the greatest element of $L$.

Proof:
Let $x, y \in S$ such that
:$x \wedge y \preceq \top$
Thus by definition of greatest element:
:$x \preceq \top$ or $y \preceq \top$
{{qed}}
Theorem: Characterization of Prime Element in Meet Semilattice

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $p \in S$,
Then:
:$p$ is prime element
{{iff}}:
:for all non-empty finite subsets $A$ of $S$:
::if $\inf A \preceq p$, then there exists element $x$ of $A$ such that $x \preceq p$.

Proof:
=== Sufficient Condition ===
Let $p$ be prime element.
Let $A$ be non-empty finite subsets of $S$.
Define
:$\map P X : \equiv X \ne \O \land \inf X \preceq p \implies \exists x \in X: x \preceq p$
where $X \subseteq S$.
We will prove that
:$\forall x \in A, B \subseteq A: \map P B \implies \map P {B \cup \set x}$
Let $x \in A, B \subseteq A$ such that
:$\map P B$
and
:$B \cup \set x \ne \O$ and $\map \inf {B \cup \set x} \preceq p$
Case $B = \O$.
By Union with Empty Set:
:$B \cup \set x = \set x$
By Infimum of Singleton:
:$\inf \set x = x$
By definition of singleton:
:$x \in \set x$
Thus
:$\exists z \in B \cup \set x: z \preceq p$
{{qed|lemma}}
Case $B \ne \O$.
By Subset of Finite Set is Finite:
:$B$ is finite.
By Existence of Non-Empty Finite Infima in Meet Semilattice:
:$B, \set x$ admit infima.
By Infimum of Infima:
:$\map \inf {B \cup \set x} = \inf B \wedge \inf \set x$
By definition of prime element:
:$\inf B \preceq p$ or $x \preceq p$
Case $\inf B \preceq p$.
By assumption:
:$\exists z \in B: z \preceq p$
By definition of union:
:$z \in B \cup \set x$
Thus
:$\exists z \in B \cup \set x: z \preceq p$
{{qed|lemma}}
Case $x \preceq p$.
By definitions of union and singleton:
:$x \in B \cup \set x$
Thus
:$\exists z \in B \cup \set x: z \preceq p$
{{qed|lemma}}
By definition of empty set:
:$\map P \O$
By Induction of Finite Set:
:$\map P A$
Thus
:if $\inf A \preceq p$, then there exists element $x$ of $A$ such that $x \preceq p$.
{{qed|lemma}}
Theorem: Isomorphism between Group Generated by Reciprocal of z and 1 minus z and Symmetric Group on 3 Letters

Let $S_3$ denote the symmetric group on $3$ letters.
Let $G$ be the group generated by $1 / z$ and $1 - z$.
Then $S_3$ and $G$ are isomorphic algebraic structures.

Proof:
Establish the mapping $\phi: S_3 \to G$ as follows:
{{begin-eqn}}
{{eqn | l = \map \phi e
      | r = z
}}
{{eqn | l = \map \phi {\paren {123} }
      | r = \dfrac 1 {1 - z}
}}
{{eqn | l = \map \phi {\paren {132} }
      | r = \dfrac {z - 1} z
}}
{{eqn | l = \map \phi {\paren {23} }
      | r = \dfrac 1 z
}}
{{eqn | l = \map \phi {\paren {13} }
      | r = 1 - z
}}
{{eqn | l = \map \phi {\paren {12} }
      | r = \dfrac z {z - 1}
}}
{{end-eqn}}
From Isomorphism by Cayley Table, the two Cayley tables can be compared by eye to ascertain that $\phi$ is an isomorphism:
Theorem: Prime Element is Meet Irreducible

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $p \in S$.
Let $p$ be a prime element of $L$.
Then $p$ is meet irreducible in $L$.

Proof:
Let $p$ be a prime element.
Let $x, y \in S$ such that
:$p = x \wedge y$
By definition of reflexivity:
:$x \wedge y \preceq p$
By definition of prime element:
:$x \preceq p$ or $y \preceq p$
By Meet Precedes Operands:
:$p \preceq x$ and $p \preceq y$
Thus by definition of antisymmetry:
:$p = x$ or $p = y$
{{qed}}
Theorem: Prime Element iff Meet Irreducible in Distributive Lattice

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a distributive lattice.
Let $p \in S$.
Then $p$ is a prime element {{iff}} $p$ is meet irreducible.

Proof:
By Prime Element is Meet Irreducible:
:if $p$ is a prime element, then $p$ is meet irreducible.
Assume that:
:$p$ is meet irreducible.
Let $x, y \in S$ such that:
:$x \wedge y \preceq p$
{{begin-eqn}}
{{eqn | l = p
      | r = p \vee \paren {x \wedge y}
      | c = Preceding iff Join equals Larger Operand
}}
{{eqn | r = \paren {p \vee x} \wedge \paren {p \vee y}
      | c = {{Defof|Distributive Lattice}}
}}
{{end-eqn}}
By definition of meet irreducible:
:$p = p \vee x$ or $p = p \vee y$
Thus by Preceding iff Join equals Larger Operand:
:$x \preceq p$ or $y \preceq p$
{{qed}}
Theorem: Multiple Equilibrium Points all have Equal Payoffs

Let $G$ be a two-person zero-sum game.
Let $G$ have more than one equilibrium point.
Then every equilibrium point of $G$ has the same payoff.

Proof:
{{proof wanted|Stated without proof, or even an explanatory comment on its scope of applicability, in Davis. This work is too vague to be useful. I am going to have to use a different work.}}
Theorem: Non-Zero-Sum Game as Zero-Sum Game

Let $G$ be a non-zero-sum game for $n$ players.
Then $G$ can be modelled as a zero-sum game for $n + 1$ players.

Proof:
At each outcome, the total payoff of $G$ will be an amount which will (for at least one outcome) not be zero
Let an $n + 1$th player be introduced to $G$ who has one move:
:$(1): \quad$ Select any player $m$.
:$(2): \quad$ If the total payoff of $G$ is $+k$, receive in payment $k$ from player $m$.
:$(3): \quad$ If the total payoff of $G$ is $-k$, pay $k$ to player $m$.
This new game is the same as $G$ but with an extra (dummy) player, and is now zero-sum.
{{qed}}
Theorem: Two-Person Zero-Sum Game is Non-Cooperative

A two-person zero-sum game necessarily has to be non-cooperative.

Proof:
A cooperative game is one where players form coalitions against the other players.
If the players in a two-person zero-sum game were to form a coalition, there would be no other players to form it against.
Further, as the total payoff is zero, there would be no benefit in collaborating on using one strategy over another, as when they pool their payoffs they are back where they started.
{{qed}}
Theorem: Simple Graph with Finite Vertex Set is Finite

Let $G$ be a simple graph.
Suppose that the vertex set of $G$ is finite.
Then $G$ is a finite graph.
That is to say, its edge set is also finite.

Proof:
Since $G$ is simple, it can have at most one edge between each two vertices.
Therefore, the mapping:
:$v: \map E G \to \powerset {\map V G}, \map v e = \set {a_e, b_e}$
which assigns to each edge its endvertices $a_e, b_e$, is an injection.
From Power Set of Finite Set is Finite and Domain of Injection Not Larger than Codomain, it follows that $\map E G$ is finite.
Hence $G$ is finite.
{{qed}}
Category:Graph Theory
Category:Simple Graphs
itanc072i6il71lvytg9hxwb3ysbn34
Theorem: Multigraph with Finite Vertex Set may not be Finite

Let $G$ be a multigraph.
Let the vertex set of $G$ be finite.
Then it is not necessarily the case that $G$ is also finite.

Proof:
{{finish|two vertices, $\N$ as edges}}
Category:Graph Theory
Category:Multigraphs
4694d4g1dnmmomeps1l1rkeh713gspp
Theorem: Modulus Larger than Real Part

:$\cmod z \ge \size {\map \Re z}$

Proof:
By the definition of a complex number, we have:
:$z = \map \Re z + i \map \Im z$
Then:
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = \sqrt {\paren {\map \Re z}^2 + \paren {\map \Im z}^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | o = \ge
      | r = \sqrt {\paren {\map \Re z}^2 }
      | c = Square of Real Number is Non-Negative, as $\map \Im z$ is real
}}
{{eqn | r = \cmod {\map \Re z}
      | c = Square of Real Number is Non-Negative, as $\map \Re z$ is real
}}
{{end-eqn}}
{{qed}}
Theorem: Modulus Larger than Imaginary Part

:$\cmod z \ge \size {\map \Im z}$

Proof:
By the definition of a complex number, we have:
:$z = \map \Re z + i \map \Im z$
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = \sqrt {\paren {\map \Re z}^2 + \paren {\map \Im z}^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | o = \ge
      | r = \sqrt {\paren {\map \Im z}^2 }
      | c = Square of Real Number is Non-Negative, as $\map \Re z$ is real
}}
{{eqn | r = \size {\map \Im z}
      | c = Square of Real Number is Non-Negative, as $\map \Im z$ is real
}}
{{end-eqn}}
{{qed}}
Theorem: Product Space is T0 iff Factor Spaces are T0

:$T$ is a $T_0$ space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_0$ space.

Proof:
=== Sufficient Condition ===
{{:Product Space is T0 iff Factor Spaces are T0/Sufficient Condition/Proof 1}}{{qed|lemma}}
Theorem: Product Space is T0 iff Factor Spaces are T0

:$T$ is a $T_0$ space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_0$ space.

Proof:
Let $T$ be a $T_0$ space.
As $S_\alpha \ne \O$ we also have $S \ne \O$ by the axiom of choice.
Let $\alpha \in I$.
From Subspace of Product Space is Homeomorphic to Factor Space, $\struct {S_\alpha, \tau_\alpha}$ is homeomorphic to a subspace $T_\alpha$ of $T$.
From $T_0$ Property is Hereditary, $T_\alpha$ is a $T_0$ space.
From $T_0$ Property is Preserved under Homeomorphism, $\struct {S_\alpha, \tau_\alpha}$ is a $T_0$ space.
As $\alpha \in I$ was arbitrary, it follows that each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_0$ space.
Theorem: Product Space is T0 iff Factor Spaces are T0

:$T$ is a $T_0$ space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_0$ space.

Proof:
Let $T$ be a $T_0$ space.
{{AimForCont}} $\exists \beta: \struct {S_\beta, \tau_\beta}$ is not a $T_0$ space.
Then $\exists a, b \in S_\beta$ such that $\forall U_\beta \in \tau_\beta$, either $a, b \in U_\beta$ or $a, b \notin U_\beta$.
Consider the elements  $y, z \in S$ defined as:
:<nowiki>$y = \family {x_\alpha} : x_\alpha = \begin {cases}
s_\alpha & : \alpha \ne \beta \\
a & : \alpha = \beta \end {cases}$</nowiki>
:<nowiki>$z = \family {x_\alpha} : x_\alpha = \begin {cases}
s_\alpha & : \alpha \ne \beta \\
b & : \alpha = \beta \end {cases}$</nowiki>
That is, $y$ and $z$ match (arbitrarily) on all coordinates except that for $\beta$.
Let $H \subseteq S: y \in H$.
Then $z \in H$ as $\forall U_\beta \in \map {\pr_\beta} H : b \in U_\beta$
Similarly, let $K \subseteq S: z \in K$.
Then $y \in K$ as $\forall U_\beta \in \map {\pr_\beta} H : a \in U_\beta$
So $T$ is not a $T_0$ space.
Hence by Proof by Contradiction it follows that each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_0$ space.
Theorem: Equivalence of Definitions of Distance to Nearest Integer Function

The following definitions of the distance to nearest integer function $\norm \cdot: \R \to \closedint 0 {\dfrac 1 2}$ are equivalent:

Proof:
Let $\alpha \in \R$, $n \in \Z$.
From Real Number is between Floor Functions:
:$\floor \alpha \le \alpha < \floor \alpha + 1$
For any $n < \floor \alpha \le \alpha$:
{{begin-eqn}}
{{eqn | l = \size {n - \alpha}
      | r = \alpha - n
      | c = {{Defof|Absolute Value}}
}}
{{eqn | o = >
      | r = \alpha - \floor \alpha
}}
{{eqn | r = \size {\alpha - \floor \alpha}
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
For any $n > \floor \alpha + 1 > \alpha$:
{{begin-eqn}}
{{eqn | l = \size {n - \alpha}
      | r = n - \alpha
      | c = {{Defof|Absolute Value}}
}}
{{eqn | o = >
      | r = \floor \alpha + 1 - \alpha
      | c = 
}}
{{eqn | r = \size {\floor \alpha + 1 - \alpha}
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \min \set {\size {n - \alpha}: n \in \Z}
      | r = \min \set {\size {\floor \alpha - \alpha}, \size {\floor \alpha + 1 - \alpha} }
      | c = Other $n$'s are disregarded by above
}}
{{eqn | r = \min \set {\alpha - \floor \alpha, \floor \alpha + 1 - \alpha}
}}
{{eqn | r = \min \set {\set \alpha, 1 - \set \alpha}
      | c = {{Defof|Fractional Part}}
}}
{{end-eqn}}
which shows that the definitions are indeed equivalent.
{{qed}}
Category:Real Analysis
mc6dwrx70vuuipe3s97te11mdqlyvuo
Theorem: Quotient and Remainder to Number Base/General Result

:$\floor {\dfrac n {b^s} } = \sqbrk {r_m r_{m - 1} \ldots r_{s + 1} r_s}_b$
and:
:$\ds n \mod {b^s} = \sum_{j \mathop = 0}^{s - 1} {r_j b^j} = \sqbrk {r_{s - 1} r_{s - 2} \ldots r_1 r_0}_b$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \frac n {b^s}
      | r = \frac {\sum_{j \mathop = 0}^m r_j b^j} {b^s}
}}
{{eqn | r = \frac {\sum_{j \mathop = 0}^{s - 1} r_j b^j} {b^s} + \sum_{j \mathop = 0}^{m - s} r_{s + j} b^j
}}
{{eqn | r = \frac {\sum_{j \mathop = 0}^{s - 1} r_j b^j} {b^s} + \sqbrk {r_m r_{m - 1} \ldots r_{s + 1} r_s}_b
      | c = {{Defof|Number Base}}
}}
{{end-eqn}}
where:
{{begin-eqn}}
{{eqn | l = \frac {\sum_{j \mathop = 0}^{s - 1} r_j b^j} {b^s}
      | o = \le
      | r = \frac {\paren {b - 1} \sum_{j \mathop = 0}^{s - 1} b^j} {b^s}
      | c = as $r_j \le b - 1$ for $\forall j$ {{hypothesis}}
}}
{{eqn | r = \frac {\paren {b^s - 1} } {b^s}
      | c = Sum of Geometric Sequence
}}
{{eqn | o = <
      | r = 1
}}
{{end-eqn}}
In particular:
:$\sqbrk {r_m r_{m - 1} \ldots r_{s + 1} r_s}_b \le \dfrac n {b^s} < \sqbrk {r_m r_{m - 1} \ldots r_{s + 1} r_s}_b + 1$
By definition of floor function:
:$\floor {\dfrac n {b^s} } = \sqbrk {r_m r_{m - 1} \ldots r_{s + 1} r_s}_b$
Finally:
{{begin-eqn}}
{{eqn | l = n \mod {b^s}
      | r = n - b^s \floor {\dfrac n {b^s} }
      | c = {{Defof|Modulo Operation}}
}}
{{eqn | r = n - b^s \sqbrk {r_m r_{m - 1} \ldots r_{s + 1} r_s}_b
      | c = as shown above
}}
{{eqn | r = n - b^s \sum_{j \mathop = 0}^{m-s} r_{s+j} b^j
      | c = {{Defof|Number Base}}
}}
{{eqn | r = n - \sum_{j \mathop = s}^m r_j b^j
}}
{{eqn | r = \sum_{j \mathop = 0}^m r_j b^j - \sum_{j \mathop = s}^m r_j b^j
      | c = {{hypothesis}}
}}
{{eqn | r = \sum_{j \mathop = 0}^{s-1} r_j b^j
}}
{{end-eqn}}
{{qed}}
Category:Number Theory
mt09v878rofnd5lrwk74mkkaigys63y
Theorem: Remainder is Primitive Recursive

Let $m, n \in \N$ be natural numbers.
Let us define the function $\rem: \N^2 \to \N$:
:<nowiki>$\map \rem {n, m} = \begin{cases}
\text{the remainder when } n \text{ is divided by } m & : m \ne 0 \\
0 & : m = 0
\end{cases}$</nowiki>
where the $\text{remainder}$ is as defined in the Division Theorem:
:If $n = m q + r$, where $0 \le r < m$, then $r$ is the remainder.
Then $\rem$ is primitive recursive.

Proof:
Let $\map \rem {n, m} = r$.
We see that as $n$ increases by $1$, then so does $r$, except when $n = m-1$ in which case increasing $n$ by $1$ makes $r$ go to $0$.
We also take into account the case where $m = 0$:
So we can define $\rem$ by cases:
:<nowiki>$\map \rem {n, m} = \begin{cases}
0 & : \map \rem {n - 1, m} = m - 1 \text { or } m = 0 \text { or } n = 0\\
\map \rem {n - 1, m} + 1 & :  \text {otherwise} \\
\end{cases}$</nowiki>
We remind ourselves of the following primitive recursive functions:
* Signum function $\sgn$
* Characteristic function of equality relation $\map {\chi_{\operatorname{eq} } } {n, m}$
* Cut-off subtraction $m \, \dot - \, n$.
We have:
* $\map \sgn m = 1 \iff m \ne 0$
* $\map {\overline \sgn} {\map {\chi_{\operatorname{eq} } } {\map \rem {n, m}, m \, \dot - \, 1} } = 1 \iff \map \rem {n, m} \ne m \, \dot - \, 1$.
So:
:$\map \sgn m \, \map {\overline \sgn} {\map {\chi_{\operatorname{eq} } } {\map \rem {n, m}, m \, \dot - \, 1} }  = 1 \iff m > 0 \land \map \rem {n, m} \ne m \, \dot - \, 1$.
So we see that:
:$\map \rem {n + 1, m} = \paren {\map \rem {n, m} + 1} \, \map \sgn m \, \map {\overline \sgn} {\map {\chi_{\operatorname{eq} } } {\map \rem {n, m}, m \, \dot - \, 1} }$
So $\rem$ is obtained by primitive recursion (over the first variable, which is allowed by Permutation of Variables of Primitive Recursive Function) from the primitive recursive functions:
* Signum function $\sgn$
* Characteristic function of equality relation $\map {\chi_{\operatorname{eq} } } {n, m}$
* Cut-off subtraction $m \, \dot - \, n$
* Addition
* Multiplication.
Thus we can use Definition by Cases is Primitive Recursive and it follows that $\rem$ is primitive recursive.
{{qed}}
Category:Remainders
Category:Primitive Recursive Functions
0b6cewu443ni0o1cjdxhbcwwlsogs84
Theorem: Quotient is Primitive Recursive

Let $m, n \in \N$ be natural numbers.
Let us define the function $\operatorname {quot}: \N^2 \to \N$:
:$\map {\operatorname {quot} } {n, m} = \begin{cases}
\text{the quotient when } n \text{ is divided by } m & : m \ne 0 \\
0 & : m = 0
\end{cases}$
where the $\text {quotient}$ and $\text {remainder}$ are as defined in the Division Theorem:
:If $n = m q + r$, where $0 \le r < m$, then $q$ is the quotient.
Then $\operatorname {quot}$ is primitive recursive.

Proof:
We note that if $m \ne 0$ and $n = m q + r$, we have:
:$\dfrac n m = q + \frac r m$
Also note that $\dfrac n m$ and $\dfrac r m$ are rational numbers and not necessarily natural numbers.
Indeed, we have:
:$0 \le \dfrac r m < 1$
So if $m > 0$ then $\map {\operatorname {quot} } {n, m}$ is the floor $\floor {\dfrac n m}$ of $\dfrac n m$.
So we have:
:$\map {\operatorname {quot} } {n, m} = \begin{cases}
0 & : m = 0 \\
\floor {\dfrac n m} & : m \ne 0
\end{cases}$
Then we see that for $m \ne 0$:
:$\floor {\dfrac {n + 1} m} = \begin {cases}
\floor {\dfrac n m} + 1 & : m \divides \paren {n + 1} \\
\floor {\dfrac n m} & : \text {otherwise}
\end {cases}$
So for $m \ne 0$:
:$\map {\operatorname {quot} } {n + 1, m} = \begin{cases}
\map {\operatorname {quot} } {n, m} + 1 & : \map \rem {n + 1, m} = 0 \\
\map {\operatorname {quot} } {n, m} & : \map \rem {n + 1, m} \ne 0
\end{cases}$
Now note that:
:$\map {\overline {\sgn} } {\map \rem {n + 1, m} } = \begin{cases}
1 & : \map \rem {n + 1, m} = 0 \\
0 & : \map \rem {n + 1, m} \ne 0
\end{cases}$
So the $\operatorname {quot}$ is defined as:
:$\map {\operatorname {quot} } {0, m} = 0$
:$\map {\operatorname {quot} } {n + 1, m} = \map \sgn m \map {\operatorname {quot} } {n, m} + \map {\overline {\sgn} } {\map \rem {n + 1, m} }$
(note that the factor $\map \sgn m$ is needed to cover the case where $m = 0$).
Thus $\operatorname {quot}$ is obtained  by primitive recursion (over the first variable, which is allowed by Permutation of Variables of Primitive Recursive Function) from the primitive recursive functions:
:Signum function $\sgn$
:Remainder $\rem$
:Addition
:Multiplication.
So it follows that $\operatorname {quot}$ is primitive recursive.
{{qed}}
Category:Primitive Recursive Functions
386u1sug1g36v2bqhi3q2uk6rb9bovp
Theorem: Tarski's Geometry is Complete/Corollary

Tarski's geometry does not contain minimal arithmetic.

Proof:
Immediate from Tarski's Geometry is Complete and the {{Corollary|Gödel's First Incompleteness Theorem}}.
{{qed}}
Category:Tarski's Geometry
6npbwztu4wi4lm1c1hnsp8vwh6u33b4
Theorem: Symmetric Relation equals its Symmetric Closure

Let $\RR$ be a symmetric relation on a set $S$.
Let $\RR^\leftrightarrow$ be the symmetric closure of $\RR$.
Then:
:$\RR = \RR^\leftrightarrow$

Proof:
{{begin-eqn}}
{{eqn | l = \RR^\leftrightarrow 
      | r = \RR \cup \RR^{-1}
      | c = {{Defof|Symmetric Closure}}
}}
{{eqn | r = \RR \cup \RR
      | c = Inverse of Symmetric Relation is Symmetric
}}
{{eqn | r = \RR
      | c = Set Union is Idempotent
}}
{{end-eqn}}
{{qed}}
Category:Symmetric Relations
Category:Symmetric Closures
50281u8vfrcqztlinlz9qtcvgzzp8km
Theorem: Not Every Two-Person Zero-Sum Game has Saddle Point

Not every two-person zero-sum game has a saddle point.

Proof:
Consider the game of Matching Pennies.
Recall its payoff table:
{{:Definition:Matching Pennies/Payoff Table}}
Trivially, by inspection, this has no entry which is the smallest entry in its row and the largest entry in its column.
{{qed}}
Theorem: Eluding Game has no Saddle Point

The eluding game has no saddle point.

Proof:
Recall the payoff table:
{{:Definition:Eluding Game/Payoff Table}}
Trivially, by inspection, this has no entry which is the smallest entry in its row and the largest entry in its column.