avewright/proofwiki-math huggingface dataset:
Theorem: External Direct Product of Projection with Canonical Injection

Let $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$ be algebraic structures with identity elements $e_1$ and $e_2$ respectively.
Let $\struct {S_1 \times S_2, \circ}$ be the external direct product of $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$
Let:
:$\pr_1: \struct {S_1 \times S_2, \circ} \to \struct {S_1, \circ_1}$ be the first projection from $\struct {S_1 \times S_2, \circ}$ to $\struct {S_1, \circ_1}$
:$\pr_2: \struct {S_1 \times S_2, \circ} \to \struct {S_2, \circ_2}$ be the second projection from $\struct {S_1 \times S_2, \circ}$ to $\struct {S_2, \circ_2}$.
Let:
:$\inj_1: \struct {S_1, \circ_1} \to \struct {S_1 \times S_2, \circ}$ be the canonical injection from $\struct {S_1, \circ_1}$ to $\struct {S_1 \times S_2, \circ}$
:$\inj_2: \struct {S_2, \circ_2} \to \struct {S_1 \times S_2, \circ}$ be the canonical injection from $\struct {S_2, \circ_2}$ to $\struct {S_1 \times S_2, \circ}$.
Then:
:$(1): \quad \pr_1 \circ \inj_1 = I_{S_1}$
:$(2): \quad \pr_2 \circ \inj_2 = I_{S_2}$
where $I_{S_1}$ and $I_{S_2}$ are the identity mappings on $S_1$ and $S_2$ respectively.

Proof:
Let $\tuple {s_1, s_2} \in S_1 \times S_2$.
So, $s_1 \in S_1$ and $s_2 \in S_2$.
From the definition of the canonical injection, we have:
:$\map {\inj_1} {s_1} = \tuple {s_1, e_2}$
:$\map {\inj_2} {s_2} = \tuple {e_1, s_2}$
From the definition of the first projection:
:$\map {\pr_1} {s_1, e_2} = s_1$
and similarly from the definition of the second projection:
:$\map {\pr_2} {e_1, s_2} = s_2$
Thus:
:$\map {\pr_1 \circ \inj_1} {s_1} = s_1$
:$\map {\pr_2 \circ \inj_2} {s_2} = s_2$
and the result follows from the definition of the identity mapping.
{{qed}}
Theorem: Inverse Completion of Natural Numbers

There exists an inverse completion of the natural numbers under addition.

Proof:
The set of natural numbers under addition can be denoted $\left ({\N, +}\right)$.
From Natural Numbers under Addition form Commutative Monoid, the algebraic structure $\left ({\N, +}\right)$ is a commutative monoid.
Therefore by definition of commutative monoid, $\left ({\N, +}\right)$ is a commutative semigroup.
From Natural Number Addition is Cancellable, all of the elements of $\left ({\N, +}\right)$ are cancellable.
The result follows from the Inverse Completion Theorem.
{{qed}}
Category:Inverse Completions
Category:Natural Numbers
q7fkui5qs8edlrc74tqw2t2cnac9r61
Theorem: L'Hôpital's Rule

Let $f$ and $g$ be real functions which are differentiable on the open interval $\openint a b$.
Let:
:$\forall x \in \openint a b: \map {g'} x \ne 0$
where $g'$ denotes the derivative of $g$ {{WRT|Differentiation}} $x$.
Let:
:$\ds \lim_{x \mathop \to a^+} \map f x = \lim_{x \mathop \to a^+} \map g x = 0$
Then:
:$\ds \lim_{x \mathop \to a^+} \frac {\map f x} {\map g x} = \lim_{x \mathop \to a^+} \frac {\map {f'} x} {\map {g'} x}$
provided that the second limit exists.

Proof:
Let $l = \ds \lim_{x \mathop \to a^+} \frac {\map {f'} x}{\map {g'} x}$.
Let $\epsilon \in \R_{>0}$.
By the definition of limit, we ought to find a $\delta \in \R_{>0}$ such that:
:$\forall x \in \R: \size {x - a} < \delta \implies \size {\dfrac {\map f x} {\map g x} - l} < \epsilon$
Fix $\delta$ such that:
:$\forall x \in \R: \size {x - a} < \delta \implies \size {\dfrac {\map {f'} x} {\map {g'} x} - l} < \epsilon$
which is possible by the definition of limit.
Define:
$\quad \map {f_0} x = \begin {cases}
\map f x & : x \in \openint a b \\
0 & : x = a
\end {cases}$
$\quad \map {g_0} x = \begin {cases}
\map g x & : x \in \openint a b \\
0 & : x = a
\end {cases}$
By definition of right-continuous, it follows that $f_0$ and $g_0$ are continuous on $\hointr a b$.
Let $x_\delta$ be such that $0 < x_\delta - a < \delta$.
We have that $f_0$ and $g_0$ are continuous on $\closedint a {x_\delta}$, and differentiable on $\openint a {x_\delta}$
Thus, by the Cauchy Mean Value Theorem with $b = x_\delta$:
:$\exists \xi \in \openint a {x_\delta}: \dfrac {\map {f'_0} \xi} {\map {g'_0} \xi} = \dfrac {\map {f_0} {x_\delta} - \map {f_0} a} {\map {g_0} {x_\delta} - \map {g_0} a}$
Since $\map {f_0} a = \map {g_0} a = 0$:
:$\exists \xi \in \openint a {x_\delta}: \dfrac {\map {f'_0} \xi} {\map {g'_0} \xi} = \dfrac {\map {f_0} {x_\delta}} {\map {g_0} {x_\delta}}$
But since $\xi, x_\delta \in \openint a b$:
:$\map {f'_0} \xi = \map {f'} \xi$
:$\map {g'_0} \xi = \map {g'} \xi$
:$\map {f_0} {x_\delta} = \map f {x_\delta}$
:$\map {g_0} {x_\delta} = \map g {x_\delta}$
Therefore:
:$\exists \xi \in \openint a {x_\delta}: \dfrac {\map {f'} \xi} {\map {g'} \xi} = \dfrac {\map f {x_\delta}} {\map g {x_\delta}}$
Now, as $a < \xi < x_\delta$, it follows that $\size{\xi - a} < \delta$ as well.
Therefore:
:$\size {\dfrac {\map f {x_\delta}} {\map g {x_\delta}} - l} = \size {\dfrac {\map {f'} \xi} {\map {g'} \xi} - l} < \epsilon$
which leads us to the desired conclusion that:
:$\ds \lim_{x \mathop \to a^+} \frac {\map f x} {\map g x} = \lim_{x \mathop \to a^+} \frac {\map {f'} x} {\map {g'} x}$
{{qed}}
Theorem: L'Hôpital's Rule

Let $f$ and $g$ be real functions which are differentiable on the open interval $\openint a b$.
Let:
:$\forall x \in \openint a b: \map {g'} x \ne 0$
where $g'$ denotes the derivative of $g$ {{WRT|Differentiation}} $x$.
Let:
:$\ds \lim_{x \mathop \to a^+} \map f x = \lim_{x \mathop \to a^+} \map g x = 0$
Then:
:$\ds \lim_{x \mathop \to a^+} \frac {\map f x} {\map g x} = \lim_{x \mathop \to a^+} \frac {\map {f'} x} {\map {g'} x}$
provided that the second limit exists.

Proof:
Take the Cauchy Mean Value Theorem with $b = x$:
:$\exists \xi \in \openint a x: \dfrac {\map {f'} \xi} {\map {g'} \xi} = \dfrac {\map f x - \map f a} {\map g x - \map g a}$
Then if $\map f a = \map g a = 0$ we have:
:$\exists \xi \in \openint a x: \dfrac {\map {f'} \xi} {\map {g'} \xi} = \dfrac {\map f x} {\map g x}$
Note that $\xi$ depends on $x$; that is, different values of $x$ may require different values of $\xi$ to make the above statement valid.
It follows from Limit of Function in Interval that $\xi \to a$ as $x \to a$.
Also, $\xi \ne a$ when $x > a$.
So from '''Hypothesis $2$''' of Limit of Composite Function, it follows that:
:$\ds \lim_{x \mathop \to a^+} \dfrac {\map {f'} \xi} {\map {g'} \xi} = \lim_{x \mathop \to a^+} \dfrac {\map {f'} x} {\map {g'} x}$
Hence the result.
{{qed}}
Theorem: Natural Numbers under Addition form Commutative Monoid

The algebraic structure $\struct {\N, +}$ consisting of the set of natural numbers $\N$ under addition $+$ is a commutative monoid whose identity is zero.

Proof:
Consider the natural numbers $\N$ defined as the naturally ordered semigroup.
From the definition of the naturally ordered semigroup, it follows that $\struct {\N, +}$ is a commutative semigroup.
From the definition of zero, $\struct {\N, +}$ has $0 \in \N$ as the identity, hence is a monoid.
{{qed}}
Theorem: Natural Numbers form Commutative Semiring

The semiring of natural numbers $\struct {\N, +, \times}$ forms a commutative semiring.

Proof:
The algebraic structure $\struct {\N, +}$ is a commutative monoid from Natural Numbers under Addition form Commutative Monoid.
Then we have:
:$(1): \quad$ Natural Number Multiplication is Closed
:$(2): \quad$ Natural Number Multiplication is Associative
:$(3): \quad$ Natural Number Multiplication is Commutative
:$(4): \quad$ Natural Number Multiplication Distributes over Addition
Thus $\struct {\N, \times}$ forms an algebraic structure which is closed such that $\times$ is associative and commutative.
So by definition, $\struct {\N, \times}$ is a commutative semigroup.
The result follows from definition of commutative semiring and the distributivity of $\times$ over $+$.
{{qed}}
Category:Natural Numbers
Category:Commutative Semirings
bqgu1mpa238fd50da2cbjl7utzy2ekt
Theorem: Integer Multiplication is Well-Defined

Integer multiplication is well-defined.

Proof:
Consider the formal definition of the integers: $x = \eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
Consider the mapping $\phi: \N_{>0} \to \Z_{>0}$ defined as:
:$\forall u \in \N_{>0}: \map \phi u = u'$
where $u' \in \Z$ is the (strictly) positive integer $\eqclass {b + u, b} {}$.
Let:
:$v' = \eqclass {c + v, c} {}$
Then:
{{begin-eqn}}
{{eqn | l = u' v'
      | r = \eqclass {b + u, b} {} \times \eqclass {c + v, c} {}
      | c = 
}}
{{eqn | r = \eqclass {\paren {b + u} \paren {c + v} + b c, \paren {b + u} c + b \paren {c + v} } {}
      | c = 
}}
{{eqn | r = \eqclass {b c + b v + c u + u v + b c, b c + u c + b c + b v} {}
      | c = 
}}
{{eqn | r = \eqclass {b c + u v, b c} {}
      | c = 
}}
{{eqn | r = \eqclass {b + u v, b} {}
      | c = 
}}
{{eqn | r = \paren {u v}'
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Multiplication is Closed

The set of integers is closed under multiplication:
:$\forall a, b \in \Z: a \times b \in \Z$

Proof:
Let us define $\eqclass {\tuple {a, b} } \boxminus$ as in the formal definition of integers.
That is, $\eqclass {\tuple {a, b} } \boxminus$ is an equivalence class of ordered pairs of natural numbers under the congruence relation $\boxminus$.
$\boxminus$ is the congruence relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxminus \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
In order to streamline the notation, we will use $\eqclass {a, b} {}$ to mean $\eqclass {\tuple {a, b} } \boxminus$, as suggested.
Integer multiplication is defined as:
:$\forall a, b, c, d \in \N: \eqclass {a, b} {} \times \eqclass {c, d} {} = \eqclass {a c + b d, a d + b c} {}$
We have that:
:$\forall a, b, c, d \in \N: \eqclass {a, b} {} \in \Z, \eqclass {c, d} {} \in \Z$
Also:
:$\forall a, b, c, d \in \N: \eqclass {a, b} {} \times \eqclass {c, d} {} = \eqclass {a c + b d, a d + b c} {}$
But:
:$a c + b d \in \N, a d + b c \in \N$
So:
:$\forall a, b, c, d \in \N: \eqclass {a c + b d, a d + b c} {} \in \Z$
Therefore integer multiplication is closed.
{{qed}}
Theorem: Integer Multiplication is Commutative

The operation of multiplication on the set of integers $\Z$ is commutative:
:$\forall x, y \in \Z: x \times y = y \times x$

Proof:
From the formal definition of integers, $\eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
Let $x = \eqclass {a, b} {}$ and $y = \eqclass {c, d} {}$ for some $x, y \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x \times y
      | r = \eqclass {a, b} {}\times \eqclass {c, d} {}
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{eqn | r = \eqclass {a c + b d, a d + b c} {}
      | c = {{Defof|Integer Multiplication}}
}}
{{eqn | r = \eqclass {c a + d b, d a + c b} {}
      | c = Natural Number Multiplication is Commutative
}}
{{eqn | r = \eqclass {c a + d b, c b + d a} {}
      | c = Natural Number Addition is Commutative
}}
{{eqn | r = \eqclass {c, d} {} \times \eqclass {a, b} {}
      | c = {{Defof|Integer Multiplication}}
}}
{{eqn | r = y \times x
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Multiplication is Associative

The operation of multiplication on the set of integers $\Z$ is associative:
:$\forall x, y, z \in \Z: x \times \paren {y \times z} = \paren {x \times y} \times z$

Proof:
From the formal definition of integers, $\eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
Let $x = \eqclass {a, b} {}$, $y = \eqclass {c, d} {}$ and $z = \eqclass {e, f} {}$ for some $x, y, z \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x \times \paren {y \times z}
      | r = \eqclass {a, b} {} \times \paren {\eqclass {c, d} {} \times \eqclass {e, f} {} }
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{eqn | r = \eqclass {a, b} {} \times \eqclass {c e + d f, c f + d e} {}
      | c = {{Defof|Integer Multiplication}}
}}
{{eqn | r = \eqclass {a \paren {c e + d f} + b \paren {c f + d e}, a \paren {c f + d e} + b \paren {c e + d f} } {}
      | c = {{Defof|Integer Multiplication}}
}}
{{eqn | r = \eqclass {a c e + a d f + b c f + b d e, a c f + a d e + b c e + b d f} {}
      | c = Natural Number Multiplication Distributes over Addition
}}
{{eqn | r = \eqclass {a c e + b d e + a d f + b c f, a c f + b d f + a d e + b c e} {}
      | c = Natural Number Addition is Commutative and Associative
}}
{{eqn | r = \eqclass {\paren {a c + b d} e + \paren {a d + b c} f, \paren {a c + b d} f + \paren {a d + b c} e} {}
      | c = Natural Number Multiplication Distributes over Addition
}}
{{eqn | r = \eqclass {a c + b d, a d + b c} {} \times \eqclass {e, f} {}
      | c = {{Defof|Integer Multiplication}}
}}
{{eqn | r = \paren {\eqclass {a, b} {} \times \eqclass {c, d} {} } \times \eqclass {e, f} {}
      | c = {{Defof|Integer Multiplication}}
}}
{{eqn | r = \paren {x \times y} \times z
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Multiplication Distributes over Addition

The operation of multiplication on the set of integers $\Z$ is distributive over addition:
:$\forall x, y, z \in \Z: x \times \paren {y + z} = \paren {x \times y} + \paren {x \times z}$
:$\forall x, y, z \in \Z: \paren {y + z} \times x = \paren {y \times x} + \paren {z \times x}$

Proof:
Let us define $\Z$ as in the formal definition of integers.
That is, $\Z$ is an inverse completion of $\N$.
From Natural Numbers form Commutative Semiring, we have that:
:All elements of $\N$ are cancellable for addition
:Addition and multiplication are commutative and associative on the natural numbers $\N$
:Natural number multiplication is distributive over natural number addition.
The result follows from the Extension Theorem for Distributive Operations.
{{qed}}
Theorem: Integer Multiplication Identity is One

The identity of integer multiplication is $1$:
:$\exists 1 \in \Z: \forall a \in \Z: a \times 1 = a = 1 \times a$

Proof:
Let us define $\eqclass {\tuple {a, b} } \boxtimes$ as in the formal definition of integers.
That is, $\eqclass {\tuple {a, b} } \boxtimes$ is an equivalence class of ordered pairs of natural numbers under the congruence relation $\boxtimes$.
$\boxtimes$ is the congruence relation defined on $\N \times \N$ by $\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$.
In order to streamline the notation, we will use $\eqclass {a, b} {}$ to mean $\eqclass {\tuple {a, b} } \boxtimes$, as suggested.
From the method of construction, $\eqclass {c + 1, c} {}$, where $c$ is any element of the natural numbers $\N$, is the isomorphic copy of $1 \in \N$.
To ease the algebra, we will take $\eqclass {1, 0} {}$ as a canonical instance of this equivalence class.
Thus it is to be shown that:
:$\forall a, b \in \N: \eqclass {a, b} {} \times \eqclass {1, 0} {} = \eqclass {a, b} {} = \eqclass {1, 0} {} \times \eqclass {a, b} {}$
From Natural Numbers form Commutative Semiring, we take it for granted that:
:addition and multiplication are commutative and associative on the natural numbers $\N$
:natural number multiplication is distributive over natural number addition.
So:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {} \times \eqclass {1, 0} {}
      | r = \eqclass {1 \times a + 0 \times b, 0 \times a + 1 \times b} {}
      | c = 
}}
{{eqn | r = \eqclass {a, b} {}
      | c = from Construction of Inverse Completion: Members of Equivalence Classes
}}
{{end-eqn}}
So:
:$\eqclass {a, b} {} \times \eqclass {1, 0} {} = \eqclass {a, b} {}$
The identity $\eqclass {a, b} {} = \eqclass {1, 0} {} \times \eqclass {a, b} {}$ is demonstrated similarly.
{{qed}}
Theorem: Integer Multiplication has Zero

The set of integers under multiplication $\struct {\Z, \times}$ has a zero element, which is $0$.

Proof:
Let us define $\eqclass {\tuple {a, b} } \boxminus$ as in the formal definition of integers.
That is, $\eqclass {\tuple {a, b} } \boxminus$ is an equivalence class of ordered pairs of natural numbers under the congruence relation $\boxminus$.
$\boxminus$ is the congruence relation defined on $\N \times \N$ by $\tuple {x_1, y_1} \boxminus \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$.
In order to streamline the notation, we will use $\eqclass {a, b} {}$ to mean $\eqclass {\tuple {a, b} } \boxminus$, as suggested.
From the method of construction, $\eqclass {c, c} {}$, where $c$ is any element of the natural numbers $\N$, is the identity of $\struct {\Z, +}$.
To ease the algebra, we will take $\eqclass {0, 0} {}$ as a canonical instance of this equivalence class.
We need to show that:
$\forall a, b, c \in \N: \eqclass {a, b} {} \times \eqclass {0, 0} {} = \eqclass {0, 0} {} = \eqclass {0, 0} {} \times \eqclass {a, b} {}$.
From Natural Numbers form Commutative Semiring, we can take it for granted that addition and multiplication are commutative on the natural numbers $\N$.
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {} \times \eqclass {0, 0} {}
      | r = \eqclass {a \times 0 + b \times 0, a \times 0 + b \times 0} {}
      | c = 
}}
{{eqn | r = \eqclass {0, 0} {}
      | c = Construction of Inverse Completion: Equivalence Class of Equal Elements
}}
{{eqn | r = \eqclass {0 \times a + 0 \times b, 0 \times a + 0 \times b} {}
      | c = 
}}
{{eqn | r = \eqclass {0, 0} {} \times \eqclass {a, b} {}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integers form Integral Domain

The set of integers $\Z$ form an integral domain under addition and multiplication.

Proof:
First we note that the integers form a commutative ring with unity whose zero is $0$ and whose unity is $1$.
Next we see that the $\struct {\Z, +, \times}$ has no divisors of zero.
So, by definition, the algebraic structure $\struct {\Z, +, \times}$ is an integral domain whose zero is $0$ and whose unity is $1$.
{{Qed}}
Theorem: Positive Integer is Well-Defined

"Positive" as applied to an integer is well-defined.

Proof:
Let us define $\eqclass {\tuple {a, b} } \boxminus$ as in the formal definition of integers.
That is, $\eqclass {\tuple {a, b} } \boxminus$ is an equivalence class of ordered pairs of natural numbers under the congruence relation $\boxminus$.
$\boxminus$ is the congruence relation defined on $\N \times \N$ by $\tuple {x_1, y_1} \boxminus \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$.
In order to streamline the notation, we will use $\eqclass {a, b} {}$ to mean $\eqclass {\tuple {a, b} } \boxminus$, as suggested.
Thus, what we are trying to prove is:
:$\eqclass {a, b} {} = \eqclass {c, d} {} \land b < a \implies d < c$
By definition:
:$\eqclass {a, b} {} = \eqclass {c, d} {} \iff a + d = b + c$
So:
{{begin-eqn}}
{{eqn | l = b
      | o = <
      | r = a
}}
{{eqn | ll= \leadsto
      | q = \exists p \in \N
      | l = a
      | r = b + p
}}
{{eqn | ll= \leadsto
      | l = b + p + d
      | r = b + c
}}
{{eqn | ll= \leadsto
      | l = p + d
      | r = c
}}
{{eqn | ll= \leadsto
      | l = d
      | o = <
      | r = c
}}
{{end-eqn}}
{{qed}}
Category:Integers
5mmpq34fhxsbpufiuwx36syjfnmi58r
Theorem: Natural Numbers are Non-Negative Integers

Let $m \in \Z$. Then:
:$(1): \quad m \in \N \iff 0 \le m$
:$(2): \quad m \in \N_{> 0} \iff 0 < m$
:$(3): \quad m \notin \N \iff -m \in \N_{> 0}$
That is, the natural numbers are precisely those integers which are greater than or equal to zero.

Proof:
Let $m \in \N$.
Then by definition of $0$:
:$0 \le m$
Conversely, let $m \in \Z: 0 \le m$.
Then:
:$\exists x, y \in \N: m = x - y$
Thus:
:$y \le m + y = x$
By Naturally Ordered Semigroup: NO 3:
:$\exists z \in \N: z + y = x = m + y$
From Naturally Ordered Semigroup: NO 2, $y$ is cancellable.
Hence:
$m = z \in \N_{> 0}$
Thus $(1)$ holds.
$(2)$ follows from $(1)$.
We infer from $(1)$ that:
:$m \notin \N \iff m < 0$
We infer from $(2)$ that:
:$-m > 0 \iff -m \in \N_{> 0}$
But by Ordering of Inverses in Ordered Monoid:
:$m < 0 \iff -m > 0$
Therefore $(3)$ also holds.
{{qed}}
Theorem: Natural Numbers are Non-Negative Integers

Let $m \in \Z$. Then:
:$(1): \quad m \in \N \iff 0 \le m$
:$(2): \quad m \in \N_{> 0} \iff 0 < m$
:$(3): \quad m \notin \N \iff -m \in \N_{> 0}$
That is, the natural numbers are precisely those integers which are greater than or equal to zero.

Proof:
Consider the formal definition of the integers: $x = \eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
Let $x \in \Z_{>0}$ be a (strictly) positive integer.
Thus by definition:
:$x > 0$
This is equivalent to the condition that $a > b$.
Hence:
:$x = \eqclass {b + u, b} {}$
for some $u \in \N_{>0}$.
It is immediate that:
:$\forall c \in \N: \eqclass {b + u, b} {} = \eqclass {c + u, c} {}$
Consider the mapping $\phi: \N_{>0} \to \Z_{>0}$ defined as:
:$\forall u \in \N_{>0}: \map \phi u = u'$
where $u' \in \Z$ be the (strictly) positive integer $\eqclass {b + u, b} {}$.
From the above we have that $\phi$ is well-defined.
Let $\eqclass {b + u, b} {} = \eqclass {c + v, c} {}$.
Then:
:$b + u + c = b + c + v$
and so:
:$u = v$
Hence $\phi$ is an injection.
Next note that all $u' \in \Z_{>0}$ can be expressed in the form:
:$u' = \eqclass {b + u, b} {}$
for arbitrary $b$.
Hence $\phi$ is a surjection.
Hence $\phi$ is an isomorphism.
By defining $\map \phi 0 = \eqclass {b, b} {}$ we see that $\N$ and $\Z_{\ge 0}$ are isomorphic.
{{qed}}
Theorem: Subtraction on Integers is Extension of Natural Numbers

Integer subtraction is an extension of the definition of subtraction on the natural numbers.

Proof:
Let $m, n \in \N: m \le n$.
From natural number subtraction, $\exists p \in \N: m + p = n$ such that $n - m = p$.
As $m, n, p \in \N$, it follows that $m, n, p \in \Z$ as well.
However, as $\Z$ is the inverse completion of $\N$, it follows that $-m \in \Z$ as well, so it makes sense to express the following:
{{begin-eqn}}
{{eqn | l = \paren {n + \paren {-m} } + m
      | r = n + \paren {\paren {-m} + m}
      | c = 
}}
{{eqn | r = n
      | c = 
}}
{{eqn | r = p + m
      | c = 
}}
{{eqn | r = \paren {n - m} + m
      | c = 
}}
{{end-eqn}}
Thus, as all elements of $\Z$ are cancellable, it follows that $n + \paren {-m} = n - m$.
So:
: $\forall m, n \in \Z, m \le n: n + \paren {-m} = n - m = n -_\N m$
and the result follows.
{{qed}}
Category:Integers
Category:Subtraction
7wy2x7ny7d5h653ngmzazw9eqd8qcub
Theorem: Non-Zero Integers are Cancellable for Multiplication

Every non-zero integer is cancellable for multiplication.
That is:
:$\forall x, y, z \in \Z, x \ne 0: x y = x z \iff y = z$

Proof:
Let $x y = x z$.
There are two cases to investigate: $x > 0$ and $x < 0$.
Let $x > 0$.
From Natural Numbers are Non-Negative Integers, $x \in \N_{> 0}$.
By the Extension Theorem for Distributive Operations and Ordering on Natural Numbers is Compatible with Multiplication, $x$ is cancellable for multiplication.
{{qed|lemma}}
Let $x < 0$.
We know that the Integers form Integral Domain and are thus a ring.
Then $-x > 0$ and so:
{{begin-eqn}}
{{eqn | l = \paren {-x} y
      | r = -\paren {x y}
      | c = Product with Ring Negative
}}
{{eqn | r = -\paren {x z}
      | c = $\struct {\Z, +}$ is a group: {{Group-axiom|3}}
}}
{{eqn | r = \paren {-x} z
      | c = Product with Ring Negative
}}
{{eqn | ll= \leadsto
      | l = y
      | r = z
      | c = from above: case where $x > 0$
}}
{{end-eqn}}
{{qed|lemma}}
So whatever non-zero value $x$ takes, it is cancellable for multiplication.
{{Qed}}
Theorem: Non-Zero Integers are Cancellable for Multiplication

Every non-zero integer is cancellable for multiplication.
That is:
:$\forall x, y, z \in \Z, x \ne 0: x y = x z \iff y = z$

Proof:
Let $y, z \in \Z: y \ne z$.
{{begin-eqn}}
{{eqn | l = y
      | o = \ne
      | r = z
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y - z
      | o = \ne
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x \paren {y - z}
      | o = \ne
      | r = 0
      | c = Ring of Integers has no Zero Divisors
}}
{{eqn | ll= \leadstoandfrom
      | l = x y - x z
      | o = \ne
      | r = 0
      | c = Integer Multiplication Distributes over Subtraction
}}
{{end-eqn}}
The result follows by transposition.
{{qed}}