avewright/proofwiki-math huggingface dataset:
Theorem: Surjection iff Right Inverse/Non-Uniqueness

A right inverse of $f$ is in general not unique.
Uniqueness occurs {{iff}} $f$ is a bijection.

Proof:
If $f$ is not an injection then:
:$\exists y \in T: \exists x_1, x_2 \in S: \map f {x_1} = y = \map f {x_2}$
Hence we have more than one choice in $\map {f^{-1} } {\set y}$ for how to map $\map g y$.
That is, $\map g y$ is not unique.
This does not happen {{iff}} $f$ is an injection.
Hence the result.
{{qed}}
Theorem: Mapping reflects Preordering

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let ${\precsim} \subseteq T \times T$ be a preordering on $T$.
Let $\RR$ be the relation defined on $S$ by the rule:
:$x \mathrel \RR y \iff \map f x \precsim \map f y$
Then $\RR$ is a preordering on $S$.

Proof:
=== Reflexivity ===
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | o = \in
      | r = T
      | c = Definition of $f$
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | o = \precsim
      | r = \map f x
      | c = as $\precsim$ is a preordering on $T$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \RR
      | r = x
      | c = Definition of $\RR$
}}
{{end-eqn}}
Thus $\RR$ is reflexive.
{{qed|lemma}}
Theorem: Bernoulli's Inequality

Let $x \in \R$ be a real number such that $x > -1$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\paren {1 + x}^n \ge 1 + n x$

Proof:
Let $0 < x < 1$.
Let $y = -x$.
Then $y > -1$ and by Bernoulli's Inequality:
:$\paren {1 + y}^n \ge 1 + n y$
Thus:
:$\paren {1 + \paren {-x} }^n \ge 1 + n \paren {-x}$
Hence the result.
{{qed}}
Theorem: Bernoulli's Inequality

Let $x \in \R$ be a real number such that $x > -1$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\paren {1 + x}^n \ge 1 + n x$

Proof:
Proof by induction:
Let $0 < x < 1$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\paren {1 - x}^n \ge 1 - n x$
=== Basis for the Induction ===
$\map P 0$ is the case:
:$\paren {1 - x}^0  = 1 \ge 1 - 0 x = 1$
so $\map P 0$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\paren {1 - x}^k \ge 1 - k x$
We need to show that:
:$\paren {1 - x}^{k + 1} \ge 1 - \paren {k + 1} x$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {1 - x}^{k + 1}
      | r = \paren {1 - x}^k \paren {1 - x}
}}
{{eqn | o = \ge
      | r = \paren {1 - k x} \paren {1 - x}
      | c = Induction Hypothesis
}}
{{eqn | r = 1 - \paren {k + 1} x + k x^2
}}
{{eqn | o = \ge
      | r = 1 - \paren {k + 1} x
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
{{qed}}
Theorem: Bernoulli's Inequality

Let $x \in \R$ be a real number such that $x > -1$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\paren {1 + x}^n \ge 1 + n x$

Proof:
Proof by induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\paren {1 + x}^n \ge 1 + nx$
=== Basis for the Induction ===
$\map P 0$ is the case:
:$\paren {1 + x}^0 \ge 1$
so $\map P 0$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\left({1 + x}\right)^k \ge 1 + kx$
We need to show that:
:$\paren {1 + x}^{k + 1} \ge 1 + \paren {k + 1} x$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {1 + x}^{k + 1}
      | r = \paren {1 + x}^k \paren {1 + x}
}}
{{eqn | o = \ge
      | r = \paren {1 + k x} \paren {1 + x}
      | c = Induction Hypothesis
}}
{{eqn | r = 1 + \paren {k + 1} x + k x^2
}}
{{eqn | o = \ge
      | r = 1 + \paren {k + 1} x
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
{{qed}}
Theorem: Bernoulli's Inequality

Let $x \in \R$ be a real number such that $x > -1$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\paren {1 + x}^n \ge 1 + n x$

Proof:
Let $y = 1 + x$.
Then $y \ge 0$, and:
:$\paren {1 + x}^n = 1 + \paren {y^n - 1}$
If $y \ge 1$, then by Sum of Geometric Sequence:
:$\ds y^n - 1 = \paren {y - 1} \sum_{k \mathop = 0}^{n - 1} y^k \ge n \paren {y - 1} = n x$
If $y < 1$, then by Sum of Geometric Sequence:
:$\ds y^n - 1 = -\paren {1 - y} \sum_{k \mathop = 0}^{n - 1} y^k \ge -n \paren {1 - y} = n x$
Hence the result.
{{qed}}
Theorem: Categories of Elements of Ring

Let $\left({R, +, \circ}\right)$ be a ring.
The elements of $R$ are partitioned into three classes:
:$(1): \quad$ the zero
:$(2): \quad$ the units
:$(3): \quad$ the proper elements.

Proof:
By definition, a proper element is a non-zero element which has no product inverse.
Also by definition, a unit is an element which does have a product inverse.
Because $0 \circ x = 0$ there can be no $x \in R$ such that $0 \times x = 1$, and so $0$ is not a unit.
Hence the result.
{{qed}}
Category:Ring Theory
76cxzcd0t4nheq7khu1x1x3rp3cc4sw
Theorem: Multiple of Ring Product

Let $\struct {R, +, \circ}$ be a ring.
Let $x, y \in \struct {R, +, \circ}$.
Then:
:$\forall n \in \Z_{> 0}: \paren {n \cdot x} \circ y = n \cdot \paren {x \circ y} = x \circ \paren {n \cdot y}$
where $n \cdot x$ denotes the $n$th multiple of $x$.

Proof:
By definition:
:$\ds n \cdot x := \sum_{j \mathop = 1}^n x$
Thus:
{{begin-eqn}}
{{eqn | l = \paren {n \cdot x} \circ y
      | r = \paren {\sum_{j \mathop = 1}^n x} \circ y
      | c = {{Defof|Integral Multiple|subdef = Rings and Fields}}
}}
{{eqn | n = 1
      | r = \sum_{j \mathop = 1}^n \paren {x \circ y}
      | c = General Distributivity Theorem
}}
{{eqn | r = n \cdot \paren {x \circ y}
      | c = {{Defof|Integral Multiple|subdef = Rings and Fields}}
}}
{{eqn | r = x \circ \paren {\sum_{j \mathop = 1}^n y}
      | c = General Distributivity Theorem from $(1)$
}}
{{eqn | r = x \circ \paren {n \cdot y}
      | c = {{Defof|Integral Multiple|subdef = Rings and Fields}}
}}
{{end-eqn}}
{{qed}}
Category:Ring Theory
m2ca2dm5x42frb8bm8zkxbfvnq9jk04
Theorem: Ordering is Preserved on Integers by Addition

The usual ordering on the integers is preserved by the operation of addition:
:$\forall a, b, c, d, \in \Z: a \le b, c \le d \implies a + c \le b + d$

Proof:
Recall that Integers form Ordered Integral Domain.
Then from Relation Induced by Strict Positivity Property is Compatible with Addition:
:$\forall x, y, z \in \Z: x \le y \implies \paren {x + z} \le \paren {y + z}$
:$\forall x, y, z \in \Z: x \le y \implies \paren {z + x} \le \paren {z + y}$
So:
{{begin-eqn}}
{{eqn | l = a
      | o = \le
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + c
      | o = \le
      | r = b + c
      | c = Relation Induced by Strict Positivity Property is Compatible with Addition
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = c
      | o = \le
      | r = d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b + c
      | o = \le
      | r = b + d
      | c = Relation Induced by Strict Positivity Property is Compatible with Addition
}}
{{end-eqn}}
Finally:
{{begin-eqn}}
{{eqn | l = a + c
      | o = \le
      | r = b + c
}}
{{eqn | l = b + c
      | o = \le
      | r = b + d
}}
{{eqn | ll= \leadsto
      | l = a + c
      | o = \le
      | r = b + d
      | c = {{Defof|Ordering}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Set of Finite Set is Finite

Let $S$ be a finite set.
Then the power set of $S$ is likewise finite.

Proof:
Let $S$ be a finite set.
Then by definition:
:$\exists n \in \N: \card S = n$
where $\card S$ denotes the cardinality of $S$.
From Cardinality of Power Set of Finite Set:
:$\card {\powerset S} = 2^n$
where $\powerset S$ denotes the power set of $S$.
As $n \in \N$ it follows that $2^n \in \N$ and so $\powerset S$ is also by definition a finite set.
{{qed}}
Category:Power Set
tikj18ioh81t6cn77m6ng7119sxrh4b
Theorem: Common Divisor Divides Difference

Let $c$ be a common divisor of two integers $a$ and $b$.
That is:
:$a, b, c \in \Z: c \divides a \land c \divides b$
Then:
:$c \divides \paren {a - b}$

Proof:
Let $c \divides a \land c \divides b$.
From Common Divisor Divides Integer Combination:
:$\forall p, q \in \Z: c \divides \paren {p a + q b}$
Putting $p = 1$ and $q = -1$:
:$c \divides \paren {a - b}$
{{qed}}
Theorem: Common Divisor Divides Difference

Let $c$ be a common divisor of two integers $a$ and $b$.
That is:
:$a, b, c \in \Z: c \divides a \land c \divides b$
Then:
:$c \divides \paren {a - b}$

Proof:
{{begin-eqn}}
{{eqn | l = c
      | o = \divides
      | r = a
}}
{{eqn | ll= \leadsto
      | q = \exists x \in \Z
      | l = a
      | r = x c
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | l = c
      | o = \divides
      | r = b
}}
{{eqn | ll= \leadsto
      | q = \exists y \in \Z
      | l = b
      | r = y c
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | ll= \leadsto
      | l = a - b
      | r = x c - y c
      | c = substituting for $a$ and $b$
}}
{{eqn | r = \paren {x - y} c
      | c = Integer Multiplication Distributes over Addition
}}
{{eqn | ll= \leadsto
      | q = \exists z \in \Z
      | l = a - b
      | r = z c
      | c = where $z = x - y$
}}
{{eqn | ll= \leadsto
      | l = c
      | o = \divides
      | r = \paren {a - b}
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Divisor Divides Multiple

Let $a, b$ be integers.
Let:
:$a \divides b$
where $\divides$ denotes divisibility.
Then:
:$\forall c \in \Z: a \divides b c$

Proof:
Let $a \divides b$.
From Integer Divides Zero:
:$a \divides 0$
Thus $a$ is a common divisor of $b$ and $0$.
From Common Divisor Divides Integer Combination:
:$\forall p, q \in \Z: a \divides \paren {p \cdot b + q \cdot 0}$
Putting $p = c$ and $q = 1$ (for example):
:$a \divides \paren {c b + 0}$
Hence the result.
{{qed}}
Theorem: Divisor Divides Multiple

Let $a, b$ be integers.
Let:
:$a \divides b$
where $\divides$ denotes divisibility.
Then:
:$\forall c \in \Z: a \divides b c$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = \divides
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in \Z
      | l = b
      | r = x a
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | ll= \leadsto
      | l = b c
      | r = x c a
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists z \in \Z
      | l = b c
      | r = z a
      | c = where $z = x c$
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \divides
      | r = b c
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
{{qed}}
Theorem: Divisor Divides Multiple

Let $a, b$ be integers.
Let:
:$a \divides b$
where $\divides$ denotes divisibility.
Then:
:$\forall c \in \Z: a \divides b c$

Proof:
We have that Integers form Integral Domain.
The result then follows from Multiple of Divisor in Integral Domain Divides Multiple.
{{qed}}
Theorem: Divisor Divides Multiple

Let $a, b$ be integers.
Let:
:$a \divides b$
where $\divides$ denotes divisibility.
Then:
:$\forall c \in \Z: a \divides b c$

Proof:
By definition, if $a \divides b$ then $\exists d \in \Z: a d = b$.
Then:
:$\paren {a d} c = b c$
that is:
:$\paren {a c} d = b c$
which follows because Integer Multiplication is Commutative and Integer Multiplication is Associative.
Hence the result.
{{qed}}
Theorem: Non-Zero Integer has Unique Positive Integer Associate

Let $a \in \Z$ be an integer such that $a \ne 0$.
Then $a$ has a unique associate $b \in \Z_{>0}$.

Proof:
Let $a \in \Z_{\ne 0}$.
By Integer Divides its Absolute Value:
:$a \divides \size a$ and $\size a \divides a$
Hence $\size a$ is an associate of $a$.
Now we prove its uniqueness.
Let $b, c \in \Z_{\ne 0}$ such that $b > 0$ and $c > 0$.
Let $a \sim b$ and $a \sim c$ where $\sim$ denotes the relation of associatehood.
By definition of associatehood:
:$a \divides b$ and $b \divides a$
and:
:$a \divides c$ and $c \divides a$
From Divisor Relation is Antisymmetric/Corollary/Proof 2:
:$a = \pm b$
and
:$a = \pm c$
That is:
:$\pm b = \pm c$
which means:
:$b = c$ or $b = -c$
But as both $b > 0$ and $c > 0$:
:$b = c$
Hence the result.
{{qed}}
Theorem: One is not Prime

The integer $1$ (one) is not a prime number.

Proof:
By definition, a prime number is a positive integer which has exactly $2$ divisors which are themselves positive integers.
From Divisors of One, the only divisors of $1$ are $1$ and $-1$.
So the only divisor of $1$ which is a positive integer is $1$.
As $1$ has only one such divisor, it is not classified as a prime number.
{{qed}}
Theorem: One is not Prime

The integer $1$ (one) is not a prime number.

Proof:
From Divisor Sum of Prime Number, the sum $\map {\sigma_1} p$ of all the positive integer divisors of a prime number $p$ is $p + 1$.
But from Divisor Sum of 1, $\map {\sigma_1} 1 = 1$.
If $1$ were to be classified as prime, then $\map {\sigma_1} 1$ would be an exception to the rule that $\map {\sigma_1} p = p + 1$.
{{qed}}
Theorem: Prefix of String is Substring

Let $S$ be a string.
Let $T$ be a prefix of $S$.
Then $T$ is a substring of $S$.

Proof:
By definition of substring, there exists a string $T'$ such that:
:$S = TT'$
Hence $S$ is the concatenation of the null string, $T$, and $T'$.
Thus by definition of substring, $T$ is a substring of $S$.
{{qed}}
Category:Prefixes
Category:Substrings
1ffntq581uimopz9dy0fh6decupnmhm
Theorem: Ring Zero is Idempotent

Let $\struct {R, +, \circ}$ be a ring whose ring zero is $0_R$.
Then $0_R$ is an idempotent element of $R$ under the ring product $\circ$:
:$0_R \circ 0_R = 0_R$

Proof:
By Ring Product with Zero (applied to $0_R$):
:$0_R \circ 0_R = 0_R$
which was to be proven. 
{{qed}}
Category:Ring Theory
aazu4uwonejgx8f8if9b80vsklxwxl1
Theorem: Prime iff Coprime to all Smaller Positive Integers

Let $p$ be a prime number.
Then:
:$\forall x \in \Z, 0 < x < p: x \perp p$
That is, $p$ is relatively prime to all smaller (strictly) positive integers.

Proof:
From Prime not Divisor implies Coprime, if $p$ does not divide an integer $x$, it is relatively prime to $x$.
From Absolute Value of Integer is not less than Divisors: Corollary, $p$ does not divide an integer smaller than $p$.
It follows that $p$ is relatively prime to all smaller (strictly) positive integers.
The special case when $x = 0$ is excluded as from Integers Coprime to Zero, $p$ is not relatively prime to $0$.
{{qed}}
Theorem: Division Theorem/Positive Divisor/Positive Dividend

<onlyinclude>
For every pair of integers $a, b$ where $a \ge 0$ and $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, a \ge 0, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
This result can be split into two parts:
Theorem: Division Theorem/Positive Divisor/Positive Dividend

<onlyinclude>
For every pair of integers $a, b$ where $a \ge 0$ and $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, a \ge 0, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
Let $a, b \in \Z$ such that $a \ge 0$ and $b > 0$ be given.
Let $S$ be defined as the set of all positive integers of the form $a - z b$ where $z$ is an integer:
:$S = \set {x \in \Z_{\ge 0}: \exists z \in \Z: x = a - z b}$
By setting $z = 0$ we have that $a \in S$.
Thus $S \ne \O$.
We have that $S$ is bounded below by $0$.
From Set of Integers Bounded Below by Integer has Smallest Element it follows that $S$ has a smallest element $r$.
Thus:
:$\exists q \in \Z: a - q b = r$
and so:
:$a = q b + r$
So we have proved the existence of $q$ and $r$ such that $a = q b + r$.
It remains to be shown that $0 \le r < b$.
We have that $r \in S$ which is bounded below by $0$.
Therefore $0 \le r$.
{{AimForCont}} $b \le r$.
So:
{{begin-eqn}}
{{eqn | l = b
      | o = \le
      | r = r
      | c = 
}}
{{eqn | o = <
      | r = r + b
      | c = as $b > 0$
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \le
      | r = r - b
      | c = 
}}
{{eqn | o = <
      | r = r
      | c = subtracting $b$ throughout
}}
{{end-eqn}}
But then:
{{begin-eqn}}
{{eqn | l = a
      | r = q b + r
      | c = from above
}}
{{eqn | ll= \leadsto
      | l = r - b
      | r = \paren {a - q b} - b
      | c = 
}}
{{eqn | r = a - b \paren {q + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r - b
      | o = \in
      | r = S
      | c = as $r - b$ is of the correct form
}}
{{end-eqn}}
But $r - b < r$ contradicts the choice of $r$ as the least element of $S$.
Hence $r < b$ as required.
Thus the existence of $q$ and $r$ satisfying $a = q b + r, 0 \le r < b$ has been demonstrated.
{{qed}}
Theorem: Division Theorem/Positive Divisor/Positive Dividend

<onlyinclude>
For every pair of integers $a, b$ where $a \ge 0$ and $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, a \ge 0, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
Let $a = 0$.
It is immediately apparent that $q = r = 0$ is the only possible solution with $0 \le r < b$.
{{qed|lemma}}
Let $a > 0$ and $b = 1$.
Then from the condition $0 \le r < b$ it follows that $r = 0$ and hence $q = a$.
{{qed|lemma}}
Let $a > 0$ and $b > 1$.
By the Basis Representation Theorem, $a$ has a unique representation to the base $b$:
{{begin-eqn}}
{{eqn | l = a
      | r = \sum_{k \mathop = 0}^s r_k b^k
      | c = 
}}
{{eqn | r = b \sum_{k \mathop = 0}^{s - 1} r_k b^{k - 1} + r_0
      | c = 
}}
{{eqn | r = b q + r
      | c = where $0 \le r = r_0 < b$
}}
{{end-eqn}}
{{qed}}
Theorem: Division Theorem/Positive Divisor/Positive Dividend

<onlyinclude>
For every pair of integers $a, b$ where $a \ge 0$ and $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, a \ge 0, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
Let $a, b \in \Z$ such that $a \ge 0$ and $b > 0$ be given.
When $a = 0$, the integers $q = r = 0$ satisfy the conditions of the theorem.
Let $a > 0$.
For each $k \in \closedint 0 {a + 1}$, let $r_k = b k$.
(Note that here, as elsewhere in this proof, $\closedint 0 {a + 1}$ denotes an integer interval.)
Then $\sequence {r_k}_{0 \mathop \le k \mathop \le a + 1}$ is a strictly increasing sequence of positive integers.
It is also the case that:
:$a + 1 \in \closedint 1 {\map b {a + 1} }$
So from Strictly Increasing Sequence induces Partition there exists $q \in \closedint 0 a$ such that:
:$a + 1 \in \closedint {r_q + 1} {r_{q + 1} }$
Let $r = a - b q$.
Then $a = b q + r$.
We have:
{{begin-eqn}}
{{eqn | l = b q + 1
      | r = r_q + 1
      | c = 
}}
{{eqn | o = \le
      | r = a + 1
      | c = 
}}
{{eqn | o = \le
      | r = r_{q + 1}
      | c = 
}}
{{eqn | r = b q + b
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | r = r
      | c = 
}}
{{eqn | r = \paren {a + 1} - \paren {b q + 1}
      | c = 
}}
{{eqn | o = \le
      | r = \paren {b q + b} - \paren {b q + 1}
      | c = 
}}
{{eqn | r = b - 1
      | c = 
}}
{{eqn | o = <
      | r = b
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Division Theorem/Positive Divisor/Positive Dividend

<onlyinclude>
For every pair of integers $a, b$ where $a \ge 0$ and $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, a \ge 0, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
Suppose $q_1, r_1$ and $q_2, r_2$ are two pairs of $q, r$ that satisfy $a = q b + r, 0 \le r < b$.
That is:
{{begin-eqn}}
{{eqn | l = a
      | r = q_1 b + r_1, 0 \le r_1 < b
      | c = 
}}
{{eqn | l = a
      | r = q_2 b + r_2, 0 \le r_2 < b
      | c = 
}}
{{end-eqn}}
This gives:
:$0 = b \paren {q_1 - q_2} + \paren {r_1 - r_2}$
{{AimForCont}} that $q_1 \ne q_2$.
{{WLOG}}, suppose that $q_1 > q_2$.
Then:
{{begin-eqn}}
{{eqn | l = q_1 - q_2
      | o = \ge
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r_2 - r_1
      | r = b \paren {q_1 - q_2}
      | c = 
}}
{{eqn | o = \ge
      | r = b \times 1
      | c = as $b > 0$
}}
{{eqn | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r_2
      | o = \ge
      | r = r_1 + b
      | c = 
}}
{{eqn | o = \ge
      | r = b
      | c = 
}}
{{end-eqn}}
This contradicts the assumption that $r_2 < b$.
A similar contradiction follows from the assumption that $q_1 < q_2$.
Therefore $q_1 = q_2$ and so $r_1 = r_2$.
Thus it follows that $q$ and $r$ are unique.
{{qed}}
Theorem: Division Theorem/Positive Divisor/Positive Dividend

<onlyinclude>
For every pair of integers $a, b$ where $a \ge 0$ and $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, a \ge 0, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
It is given by Division Theorem: Positive Divisor: Positive Dividend: Existence that such $q$ and $r$ exist.
Let $a = 0$.
It is immediately apparent that $q = r = 0$ is the only possible solution with $0 \le r < b$.
{{qed|lemma}}
Let $a > 0$ and $b = 1$.
Then from the condition $0 \le r < b$ it follows that $r = 0$.
Hence $r = 0, q = a$ is the only possible solution.
{{qed|lemma}}
Let $a > 0$ and $b > 1$.
By the Basis Representation Theorem, $a$ has a unique representation to the base $b$:
{{begin-eqn}}
{{eqn | l = a
      | r = \sum_{k \mathop = 0}^s r_k b^k
      | c = 
}}
{{eqn | r = b \sum_{k \mathop = 0}^{s - 1} r_k b^{k - 1} + r_0
      | c = 
}}
{{eqn | r = b q + r
      | c = where $0 \le r = r_0 < b$
}}
{{end-eqn}}
Suppose a second pair $q', r'$ were to exist.
Then there would be a representation for $q'$ to the base $b$:
:$\displaystyle q' = \sum_{k \mathop = 0}^t u_k b^k$
so that:
{{begin-eqn}}
{{eqn | l = a
      | r = b q' + r'
      | c = $0 \le r < b$
}}
{{eqn | r = \sum_{k \mathop = 0}^t u_k b^{k + 1} + r'
      | c = 
}}
{{end-eqn}}
But there already exists a representation of $a$ to the base $b$:
:$\displaystyle a = \sum_{k \mathop = 0}^s r_k b^k$
By the Basis Representation Theorem, such a representation is unique.
So:
{{begin-eqn}}
{{eqn | l = t
      | r = s - 1
}}
{{eqn | l = u_k
      | r = r_{k + 1}
}}
{{eqn | l = r'
      | r = a_0
}}
{{eqn | r = r
}}
{{end-eqn}}
and hence $q' = q$.
{{qed}}
Theorem: Division Theorem/Positive Divisor

<onlyinclude>
For every pair of integers $a, b$ where $b > 0$, there exist unique integers $q, r$ such that $a = q b + r$ and $0 \le r < b$:
:$\forall a, b \in \Z, b > 0: \exists! q, r \in \Z: a = q b + r, 0 \le r < b$
<onlyinclude>
In the above equation:
:$a$ is the '''dividend'''
:$b$ is the '''divisor'''
:$q$ is the '''quotient'''
:$r$ is the '''principal remainder''', or, more usually, just the '''remainder'''.

Proof:
This result can be split into two parts: