avewright/proofwiki-math huggingface dataset:
Theorem: Quadratic Integers over 2 form Subdomain of Reals

Let $\Z \sqbrk {\sqrt 2}$ denote the set of quadratic integers over $2$:
:$\Z \sqbrk {\sqrt 2} := \set {a + b \sqrt 2: a, b \in \Z}$
That is, all numbers of the form $a + b \sqrt 2$ where $a$ and $b$ are integers.
Then the algebraic structure:
:$\struct {\Z \sqbrk {\sqrt 2}, +, \times}$
where $+$ and $\times$ are conventional addition and multiplication on real numbers, form an integral subdomain of the real numbers $\R$.

Proof:
From Integers form Subdomain of Reals, $\struct {\Z, +, \times}$ is an integral subdomain of the real numbers $\R$.
We have that $\sqrt 2 \in \R$.
Every expression of the form:
:$a_0 + a_1 \sqrt 2 + a_2 \paren {\sqrt 2}^2 + \cdots + a_n \paren {\sqrt 2}^n$
can be simplified to a number of the form $a + b \sqrt 2$, where $a, b \in \Z$.
The result follows from Set of Polynomials over Integral Domain is Subring.
Theorem: Sufficient Conditions for Uncountability

Let $X$ be a set.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$X$ contains an uncountable subset}}
{{item|(2):|$X$ is uncountable}}
{{item|(3):|Every sequence of distinct points $\sequence {x_n}_{n \mathop \in \N}$ in $X$ omits at least one $x \in X$}}
{{item|(4):|There is no surjection $\N \twoheadrightarrow X$}}
{{item|(5):|$X$ is infinite and there is no bijection $X \leftrightarrow \N$}}
{{end-itemize}}
Assuming the Continuum Hypothesis holds, we also have the equivalent uncountability condition:
:$(6): \quad $There exist extended real numbers $a < b$ and a surjection $X \to \closedint a b$

Proof:
{{Recall|Uncountable Set|uncountable set}}
:$X$ is uncountable {{iff}} there is no injection $X \hookrightarrow \N$.
Theorem: Direct Product iff Nontrivial Idempotent

Let $\struct {R, +, \circ}$ be a commutative ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Then $R$ is the direct product of two non-trivial rings {{iff}} $R$ contains an idempotent element not equal to $0_R$ or $1_R$.

Proof:
=== Necessary Condition ===
Suppose $R_1$ and $R_2$ are non-trivial rings, such that $R = R_1 \times R_2$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {1_{R_1}, 0_{R_2} }^2
      | r = \tuple {1_{R_1}^2, 0_{R_2}^2}
      | c = 
}}
{{eqn | r = \tuple {1_{R_1}, 0_{R_2} }
      | c = 
}}
{{end-eqn}}
Thus $\tuple {1_{R_1}, 0_{R_2} }$ is an idempotent element of $R$ not equal to $0_R$ or $1_R$.
{{qed|lemma}}
Theorem: Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive

Let $\struct {D, +, \times, \le}$ be an ordered integral domain whose zero is $0_D$.
Then:
:$\forall x \in D: x \ne 0_D \iff \map P {x \times x}$
where $\map P {x \times x}$ denotes that $x \times x$ has the (strict) positivity property.
That is, the square of any element of an ordered integral domain is (strictly) positive {{iff}} that element is non-zero.

Proof:
Let $x = 0_D$.
Then $x \times x = 0_D \times 0_D = 0_D$ by the properties of the ring zero.
Thus by definition of strict positivity property:
:$\neg \map P {0_D \times 0_D}$
{{qed|lemma}}
Now suppose $x \ne 0_D$.
One of two cases applies:
:$\map P x$
:$\neg \map P x$
Let $\map P x$.
Then by definition of (strict) positivity:
:$\map P {x \times x}$
Now suppose $\neg \map P x$.
Then by the trichotomy law of ordered integral domains:
:$\map P {-x}$
Then again by definition:
:$\map P {\paren {-x} \times \paren {-x} }$.
But by Product of Ring Negatives:
:$\paren {-x} \times \paren {-x} = x \times x$
So again:
:$\map P {x \times x}$
Hence the result.
{{qed}}
Theorem: Unity of Ordered Integral Domain is Strictly Positive

Let $\struct {D, +, \times \le}$ be an ordered integral domain whose unity is $1_D$.
Then:
:$\map P {1_D}$
where $P$ is the (strict) positivity property.

Proof:
We have by definition of the unity that:
:$\forall a \in D: 1_D \times a = a = a \times 1_D$
This particularly applies to $1_D$ itself:
:$1_D = 1_D \times 1_D$
But then by Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive:
:$\map P {1_D \times 1_D} \implies \map P {1_D}$
{{qed}}
Theorem: Integers form Ordered Integral Domain

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

Proof:
From Integers form Integral Domain we have that $\struct {\Z, +, \times}$ forms an integral domain.
From Natural Numbers are Non-Negative Integers we have that the set $\N$ can be considered as a subset of the integers.
Then we have that $\struct {\N_{>0}, +, \times}$ is a (commutative) semiring.
So it follows by definition of semiring, in particular the fact that $+$ and $\times$ on $\N_{> 0}$ are closed, that:
:$\forall a, b \in \N_{> 0}: a + b \in \N_{>0}$
:$\forall a, b \in \N_{> 0}: a \times b \in \N_{>0}$
It follows that we can define a property $P$ on $\Z$ such that:
:$\forall x \in \Z: \map P x \iff x \in \N_{>0}$
Checking that $P$ fulfils the conditions for it to be the (strict) positivity property:
:$(1): \quad \forall a, b \in \Z: \map P a \land \map P b \implies \map P {a + b}$
Follows directly from the fact that $\map P x \iff x \in \N_{> 0}$.
:$(2): \quad \forall a, b \in \Z: \map P a \land \map P b \implies \map P {a \times b}$
Follows directly from the fact that $\map P x \iff x \in \N_{> 0}$.
:$(3): \quad \forall a \in \Z: \map P a \lor \map P {-a} \lor a = 0$
This follows from the definition of the integers as the Inverse Completion of Natural Numbers.
If $a \in \Z - \N$ then $\exists b \in \N: a + b = 0$ and so $a = -b$.
Hence the conditions are fulfilled and $\struct {\Z, +, \times}$ forms an ordered integral domain.
{{qed}}
Theorem: Integers form Ordered Integral Domain

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

Proof:
From Integers form Integral Domain we have that $\struct {\Z, +, \times}$ forms an integral domain.
From Integers form Totally Ordered Ring, $\struct {\Z, +, \times}$ is a totally ordered ring.
Hence the result.
{{qed}}
Theorem: Rational Numbers form Ordered Integral Domain

The rational numbers $\Q$ form an ordered integral domain under addition and multiplication.

Proof:
This follows directly from Rational Numbers form Totally Ordered Field:
The set of rational numbers $\Q$ forms an ordered field under addition and multiplication: $\struct {\Q, +, \times, \le}$.
An ordered field is also an ordered integral domain.
{{Qed}}
Theorem: Real Numbers form Ordered Integral Domain

The set of real numbers $\R$ forms an ordered integral domain under addition and multiplication: $\struct {\R, +, \times, \le}$.

Proof:
This follows directly from Real Numbers form Totally Ordered Field.
The set of real numbers $\R$ forms an ordered field under addition and multiplication: $\struct {\R, +, \times, \le}$.
An ordered field is also an ordered integral domain.
{{Qed}}
Theorem: Real Numbers form Ordered Integral Domain

The set of real numbers $\R$ forms an ordered integral domain under addition and multiplication: $\struct {\R, +, \times, \le}$.

Proof:
We have that the real numbers $\struct {\R, +, \times}$ form an integral domain.
It remains to specify a property $P$ on $\R$ such that:
:$(1): \quad \forall a, b \in \R: \map P a \land \map P b \implies \map P {a + b}$
:$(2): \quad \forall a, b \in \R: \map P a \land \map P b \implies \map P {a \times b}$
:$(3): \quad \forall a \in \R: \map P a \lor \map P {-a} \lor a = 0$
We have that the integers $\struct {\Q, +, \times}$ form an ordered integral domain, where $\Q$ denotes the set of rational numbers.
Let $P'$ be the (strict) positivity property on $\struct {\Q, +, \times}$.
Let us define the property $P$ on $\R$ as:
:$\forall a \in \R: \map P a \iff a = \eqclass {\sequence {a_n} } {}: \forall n \in \N: \map {P'} {a_n}$
That is, an element $a = \eqclass {\sequence {a_n} } {}$ has $P$ {{iff}} $a_n$ has (strict) positivity property in $\Q$ for all $n \in \N$.
Now let $a = \eqclass {\sequence {a_n} } {}$ and $b = \eqclass {\sequence {b_n} } {}$ such that $\map P a$ and $\map P b$.
Then by definition of real addition:
:$\eqclass {\sequence {a_n} } {} + \eqclass {\sequence {b_n} } {} = \eqclass {\sequence {a_n + b_n} } {}$
and real multiplication:
:$\eqclass {\sequence {a_n} } {} \times \eqclass {\sequence {b_n} } {} = \eqclass {\sequence {a_n \times b_n} } {}$
It can be seen from the definition of (strict) positivity $P'$ on $\Q$ that $\map P {a + b}$ and $\map P {a \times b}$.
It can be seen that if $\map P a$ then $\neg \map P {-a}$ and vice versa.
Also we note that $\neg \map P 0$ and of course $\neg \map P {-0}$.
So the property $P$ we defined fulfils the criteria for the (strict) positivity property.
Hence the result.
{{qed}}
Theorem: Quadratic Integers over 2 form Ordered Integral Domain

Let $\Z \sqbrk {\sqrt 2}$ denote the set of quadratic integers over $2$:
:$\Z \sqbrk {\sqrt 2} := \set {a + b \sqrt 2: a, b \in \Z}$
that is, all numbers of the form $a + b \sqrt 2$ where $a$ and $b$ are integers.
Then the algebraic structure:
:$\struct {\Z \sqbrk {\sqrt 2}, +, \times}$
where $+$ and $\times$ are conventional addition and multiplication on real numbers, is an ordered integral domain.

Proof:
We have that Quadratic Integers over 2 form Subdomain of Reals.
We also have that such numbers are real.
The result follows from Real Numbers form Ordered Integral Domain.
{{explain|So is a subdomain of an ordered integral domain always an ordered integral domain? Does this need to be proved?}}
{{qed}}
Theorem: General Positivity Rule in Ordered Integral Domain

Let $\struct {D, +, \times}$ be an ordered integral domain, whose (strict) positivity property is denoted $P$.
Let $S \subset D$ be a subset of $D$ such that:
:$\forall s \in S: \map P x$
Then the following are true:
:$\ds \forall n \in \N_{>0}: \forall s_i \in S: \map P {\sum_{i \mathop = 1}^n s_i}$
:$\ds \forall n \in \N_{>0}: \forall s_i \in S: \map P {\prod_{i \mathop = 1}^n s_i}$
where:
:$\ds \sum_{i \mathop = 1}^n s_i = s_1 + s_2 + \cdots + s_n$
:$\ds \prod_{i \mathop = 1}^n s_i = s_1 \times s_2 \times \cdots \times s_n$
That is, the ring sum and ring product of any number of elements in $D$ which have the (strict) positivity property also have the (strict) positivity property.

Proof:
Trivially true for $n = 1$, and true by definition for $n = 2$.
Suppose it is true for all $n$ up to $n = k$ for some $k \in \N$.
Then:
:$\ds \forall s_i \in S: \map P {\sum_{i \mathop = 1}^k s_i}$
:$\ds \forall s_i \in S: \map P {\prod_{i \mathop = 1}^k s_i}$
Take any $\ds \sum_{i \mathop = 1}^{k + 1} s_i = \sum_{i \mathop = 1}^k s_i + s_{k + 1}$.
Then:
:$\ds \map P {\sum_{i \mathop = 1}^k s_i}$ and $\map P {s_{k + 1} }$
so:
:$\ds \map P {\sum_{i \mathop = 1}^{k + 1} s_i}$
because the (strict) positivity property holds for all $s_i \in S$.
Similarly:
:$\ds \map P {\prod_{i \mathop = 1}^k s_i}$ and $\map P {s_{k + 1} }$
so:
:$\ds \map P {\prod_{i \mathop = 1}^{k + 1} s_i}$
The result follows by the Principle of Complete Induction.
{{qed}}
Theorem: Finite Integral Domain cannot be Ordered

Let $\struct {D, +, \times}$ be an integral domain whose unity is $1_D$ and whose order is finite.
Then $D$ cannot be an ordered integral domain.

Proof:
Let $\struct {D, +, \times}$ be an integral domain whose order is $n$.
{{AimForCont}} there exists a (strict) positivity property $P$ on $\struct {D, +, \times}$.
From Unity of Ordered Integral Domain is Strictly Positive, we have that $\map P {1_D}$.
Let $\struct {D, +}$ be the additive group of $\struct {D, +, \times}$.
From Order of Element Divides Order of Finite Group, the order of $1_D$ is also finite.
So:
:$\exists m \in \N: m \cdot 1_D = 0_D$
where $0_D$ is the zero of $D$.
But then from the General Positivity Rule in Ordered Integral Domain that would mean $\map P {0_D}$ which contradicts the trichotomy law of the positivity property.
Further, note that from Inverse Element is Power of Order Less 1 we have that $-1_D = \paren {m - 1} \cdot 1_D$.
But from the General Positivity Rule in Ordered Integral Domain $\map P {\paren {m - 1} \cdot 1_D}$ and so $\map P {-1_D}$ which is an even more dramatic way of showing that the trichotomy law of the positivity property is contradicted.
Hence an integral domain whose order is finite can not be ordered.
{{qed}}
Theorem: Ring of Integers Modulo m cannot be Ordered Integral Domain

Let $m \in \Z: m \ge 2$.
Let $\struct {\Z_m, +, \times}$ be the ring of integers modulo $m$.
Then $\struct {\Z_m, +, \times}$ cannot be an ordered integral domain.

Proof:
First note that from Ring of Integers Modulo Prime is Integral Domain, $\struct {\Z_m, +, \times}$ is an integral domain only when $m$ is prime.
So for $m$ composite the result holds.
If $m$ is prime, and $\struct {\Z_m, +, \times}$ is therefore an integral domain, its order is finite. 
The result follows from Finite Integral Domain cannot be Ordered.
{{qed}}
Theorem: Strict Positivity Property induces Total Ordering

Let $\struct {D, +, \times}$ be an integral domain whose zero is $0_D$.
Let $D$ be endowed with a (strict) positivity property $P: D \to \set {\T, \F}$.
Then there exists a total ordering $\le$ on $\struct {D, +, \times}$ induced by $P$ which is compatible with the ring structure of $\struct {D, +, \times}$.

Proof:
By definition of the strict positivity property:
{{:Definition:Strict Positivity Property}}
Let us define a relation $<$ on $D$ as:
:$\forall a, b \in D: a < b \iff \map P {-a + b}$
Setting $a = 0$:
:$\forall b \in D: 0 < b \iff \map P b$
demonstrating that (strictly) positive elements of $D$ are those which are greater than zero.
From Relation Induced by Strict Positivity Property is Compatible with Addition we have that $<$ is compatible with $+$.
From Relation Induced by Strict Positivity Property is Transitive we have that $<$ is transitive.
From Relation Induced by Strict Positivity Property is Asymmetric and Antireflexive we have that $<$ is asymmetric and antireflexive.
Thus by definition, $<$ is a strict ordering.
Let the relation $\le$ be defined as the reflexive closure of $<$.
From Reflexive Closure of Strict Ordering is Ordering we have that $\le$ is an ordering on $D$.
From Relation Induced by Strict Positivity Property is Trichotomy, and from the Trichotomy Law (Ordering), we have that $\le$ is a total ordering.
Hence the result.
{{qed}}
Theorem: Relation Induced by Strict Positivity Property is Transitive

Let $\struct {D, +, \times}$ be an ordered integral domain where $P$ is the (strict) positivity property.
Let the relation $<$ be defined on $D$ as:
:$\forall a, b \in D: a < b \iff \map P {-a + b}$
Then $<$ is a transitive relation.

Proof:
Let $a < b$ and $b < c$.
Thus:
{{begin-eqn}}
{{eqn | o = 
      | r = a < b, b < c
      | c = 
}}
{{eqn | o = \leadsto
      | r = \map P {-a + b}, \map P {-b + c}
      | c = Definition of $<$
}}
{{eqn | o = \leadsto
      | r = \map P {\paren {-a + b} + \paren {-b + c} }
      | c = {{Defof|Strict Positivity Property}}
}}
{{eqn | o = \leadsto
      | r = \map P {-a + c}
      | c = Properties of $+$ in $D$
}}
{{eqn | o = \leadsto
      | r = a < c
      | c = Definition of $<$
}}
{{end-eqn}}
And so $<$ is seen to be transitive.
{{qed}}
Theorem: Relation Induced by Strict Positivity Property is Compatible with Addition

Let $\struct {D, +, \times}$ be an ordered integral domain where $P$ is the (strict) positivity property.
Let the relation $<$ be defined on $D$ as:
:$\forall a, b \in D: a < b \iff \map P {-a + b}$
Then $<$ is compatible with $+$, that is:
:$\forall x, y, z \in D: x < y \implies \paren {x + z} < \paren {y + z}$
:$\forall x, y, z \in D: x < y \implies \paren {z + x} < \paren {z + y}$

Proof:
Let $a < b$:
{{begin-eqn}}
{{eqn | o = 
      | r = a < b
      | c = 
}}
{{eqn | o = \leadsto
      | r = \map P {-a + b}
      | c = by definition of $<$
}}
{{eqn | o = \leadsto
      | r = \map P {-a + b + \paren {-c} + c}
      | c = for any $c \in D$
}}
{{eqn | o = \leadsto
      | r = \map P {\paren {-a + \paren {-c} } + \paren {b + c} }
      | c = properties of $+$ in $D$
}}
{{eqn | o = \leadsto
      | r = \map P {-\paren {a + c} + \paren {b + c} }
      | c = properties of $+$ in $D$
}}
{{eqn | o = \leadsto
      | r = a + c < b + c
      | c = by definition of $<$
}}
{{eqn | o = \leadsto
      | r = c + a < c + b
      | c = commutativity of $+$
}}
{{end-eqn}}
And so $<$ is seen to be compatible with $+$.
{{qed}}
Theorem: Relation Induced by Strict Positivity Property is Compatible with Multiplication

Let $\struct {D, +, \times}$ be an ordered integral domain where $P$ is the (strict) positivity property.
Let the relation $<$ be defined on $D$ as:
:$\forall a, b \in D: a < b \iff \map P {-a + b}$
Then $<$ is compatible with $\times$ in the following sense:
:$\forall x, y, z \in D: x < y, \map P z \implies \paren {z \times x} < \paren {z \times y}$
:$\forall x, y, z \in D: x < y, \map P z \implies \paren {x \times z} < \paren {y \times z}$

Proof:
If $x < y$ then $\map P {-x + y}$.
Hence:
{{begin-eqn}}
{{eqn | o = 
      | r = \map P {-x + y}, \, \map P z
      | c = 
}}
{{eqn | o = \leadsto
      | r = \map P {z \times \paren {-x + y} }
      | c = {{Defof|Strict Positivity Property}}
}}
{{eqn | o = \leadsto
      | r = \map P {-z \times x + z \times y}
      | c = Distributivity of $\times$ over $+$
}}
{{eqn | o = \leadsto
      | r = z \times x < z \times y
      | c = 
}}
{{end-eqn}}
The other result follows from the fact that $\times$ is commutative in an integral domain.
{{qed}}
Theorem: Relation Induced by Strict Positivity Property is Trichotomy

Let $\struct {D, +, \times}$ be an ordered integral domain where $P$ is the (strict) positivity property.
Let the relation $<$ be defined on $D$ as:
:$\forall a, b \in D: a < b \iff \map P {-a + b}$
Then $\forall a, b \in D:$ exactly one of the following conditions applies:
:$a < b$
:$a = b$
:$a > b$
That is, $<$ is a trichotomy.

Proof:
Take any $a, b \in D$ and consider $-a + b$.
From the trichotomy law of ordered integral domains, exactly one of the following applies:
:$(1): \quad \map P {-a + b}$
:$(2): \quad \map P {-\paren {-a + b} }$
:$(3): \quad -a + b = 0$
Taking each of these in turn and taking into account that $\struct {D, +}$ is the additive group of $\struct {D, +, \times}$:
{{begin-eqn}}
{{eqn | n = 1
      | o = 
      | r = \map P {-a + b}
      | c = 
}}
{{eqn | o = \leadsto
      | r = a < b
      | c = Definition of $<$
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | n = 2
      | o = 
      | r = \map P {-\paren {-a + b} }
      | c = 
}}
{{eqn | o = \leadsto
      | r = \map P {-b + a}
      | c = 
}}
{{eqn | o = \leadsto
      | r = b < a
      | c = Definition of $<$
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | n = 3
      | o = 
      | r = -a + b = 0
      | c = 
}}
{{eqn | o = \leadsto
      | r = a = b
      | c = adding $a$ to both sides
}}
{{end-eqn}}
{{qed|lemma}}
The result has been proved.
{{qed}}
Theorem: Relation Induced by Strict Positivity Property is Asymmetric and Antireflexive

Let $\struct {D, +, \times}$ be an ordered integral domain where $P$ is the (strict) positivity property.
Let the relation $<$ be defined on $D$ as:
:$\forall a, b \in D: a < b \iff \map P {-a + b}$
Then $<$ is asymmetric and antireflexive.

Proof:
From the trichotomy law of ordered integral domains, for all $x \in D$ exactly one of the following applies:
:$(1): \quad \map P x$
:$(2): \quad \map P {-x}$
:$(3): \quad x = 0$
Let $a, b \in D: a < b$.
Then by definition:
:$\map P {-a + b}$
Suppose also that $b < a$.
Then by definition:
:$\map P {-b + a}$
and so:
:$\map P {-\paren {-a + b} }$
But then that contradicts the trichotomy law of ordered integral domains:
Either:
:$(1): \quad \map P {-a + b}$
or:
:$(2): \quad \map P {-\paren {-a + b} }$
So $(1)$ and $(2)$ can not both apply, and so if $a < b$ it is not possible that $b < a$.
Thus $<$ is asymmetric.
Now suppose $\exists a \in D: a < a$.
Then that would mean $\map P {-a + a}$, that is, $\map P {0_D}$.
But this also contradicts the conditions of the trichotomy law of ordered integral domains.
Hence:
:$\forall a \in D: a \not < a$
and so $<$ is antireflexive.
{{qed}}
Category:Ordered Integral Domains
7wj0qad5d2yz9f13et7dv0yx2k16dak
Theorem: Absolute Value on Ordered Integral Domain is Strictly Positive except when Zero

Let $\struct {D, +, \times, \le}$ be an ordered integral domain.
For all $a \in D$, let $\size a$ denote the absolute value of $a$.
Then $\size a$ is (strictly) positive except when $a = 0$.

Proof:
Let $P$ be the (strict) positivity property on $D$.
Let $<$ be the (strict) total ordering defined on $D$ as:
:$a < b \iff a \le b \land a \ne b$
From the trichotomy law, exactly one of three possibilities holds for any $ a \in D$:
$(1): \quad \map P a$:
In this case $0 < a$ and so $\size a = a$.
So:
:$\map P a \implies \map P {\size a}$
$(2): \quad \map P {-a}$:
In this case $a < 0$ and so $\size a = -a$.
So:
:$\map P {-a} \implies \map P {\size a}$
$(3): \quad a = 0$:
In this case $\size a = a$.
So:
:$a = 0 \implies \size a = 0$.
Hence the result.
{{qed}}
Theorem: Sum of Absolute Values on Ordered Integral Domain

Let $\struct {D, +, \times, \le}$ be an ordered integral domain.
For all $a \in D$, let $\size a$ denote the absolute value of $a$.
Then:
:$\size {a + b} \le \size a + \size b$

Proof:
Let $P$ be the (strict) positivity property on $D$.
Let $<$ be the (strict) total ordering defined on $D$ as:
:$a < b \iff a \le b \land a \ne b$
Let $N$ be the (strict) negativity property on $D$.
Let $a \in D$.
If $\map P a$ or $a = 0$ then $a \le \size a$.
If $\map N a$ then by Properties of Strict Negativity: $(1)$ and definition of absolute value:
:$a < 0 < \size a$
and hence by transitivity $<$ we have:
:$a < \size a$
By similar reasoning:
:$-a < \size a$
Thus for all $a, b \in D$ we have:
:$a \le \size a, b \le \size b$
As $<$ is compatible with $+$, we have:
:$a + b \le \size a + \size b$
and:
:$-\paren {a + b} = \paren {-a} + \paren {-b} \le \size a + \size b$
But either:
:$\size {a + b} = a + b$
or:
:$\size {a + b} = -\paren {a + b}$
Hence the result:
:$\size {a + b} \le \size a + \size b$
{{qed}}
Theorem: One Succeeds Zero in Well-Ordered Integral Domain

Let $\struct {D, +, \times, \le}$ be a well-ordered integral domain.
Let $0$ and $1$ be the zero and unity respectively of $D$.
Then $0$ is the immediate predecessor of $1$:
:$0 < 1$
:$\neg \exists a \in D: 0 < a < 1$

Proof:
{{AimForCont}} there exists an element $a \in D$ such that $0 < a < 1$.
Let us create the set $S$ of all such elements:
:$S = \set {x \in D: 0 < x < 1}$
We know $S$ is not empty because it has already been asserted that $a$ is in it.
And all the elements in $S$ are strictly positive by definition.
Because $D$ is well-ordered it follows that $S$ has a minimal element, which we will call $m$.
Thus we have $0 < m < 1$.
Then from Square of Element Less than Unity in Ordered Integral Domain we have:
:$0 < m \times m < m$
Thus $m \times m \in S$ is an element of $S$ which is smaller than $m$.
But $m$ was supposed to be the minimal element of $S$.
From this contradiction we deduce that there can be no such element $a$ such that $0 < a < 1$.
{{qed}}
Theorem: Square of Element Less than Unity in Ordered Integral Domain

Let $\struct {D, +, \times, \le}$ be an ordered integral domain.
Let $x \in D$ such that $0 < x < 1$.
Then:
: $0 < x \times x < x$

Proof:
We have that $0 < x < 1$.
From Relation Induced by Strict Positivity Property is Compatible with Multiplication:
:$0 \times x < x \times x < 1 \times x$
Hence the result.
{{qed}}
Category:Ordered Integral Domains
payuibiqj3z0g90g32oa6vktwe0b6lr