Strict Ordering on Integers is Trichotomy

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\eqclass {a, b} {}$ and $\eqclass {c, d} {}$ be integers, as defined by the formal definition of integers.

Then exactly one of the following holds:

\(\ds \eqclass {a, b} {}\) \(<\) \(\ds \eqclass {c, d} {}\)
\(\ds \eqclass {a, b} {}\) \(=\) \(\ds \eqclass {c, d} {}\)
\(\ds \eqclass {a, b} {}\) \(>\) \(\ds \eqclass {c, d} {}\)

That is, strict ordering is a trichotomy.


Proof

By the formal definition of integers, we have that $a, b, c, d, e, f$ are all natural numbers.

To eliminate confusion between integer ordering and the ordering on the natural numbers, let $a \preccurlyeq b$ denote that the natural number $a$ is less than or equal to the natural number $b$.


We have:

\(\ds \eqclass {a, b} {}\) \(<\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds \eqclass {c, d} {}\) \(\nless\) \(\ds \eqclass {a, b} {}\) Strict Ordering on Integers is Asymmetric

Then:

\(\ds \eqclass {a, b} {}\) \(<\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\prec\) \(\ds b + c\) Definition of Strict Ordering on Integers
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\ne\) \(\ds b + c\) Definition of Ordering on Natural Numbers
\(\ds \leadsto \ \ \) \(\ds \eqclass {a, b} {}\) \(\ne\) \(\ds \eqclass {c, d} {}\) Definition of Strict Ordering on Integers


Similarly:

\(\ds \eqclass {a, b} {}\) \(>\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds \eqclass {c, d} {}\) \(\ngtr\) \(\ds \eqclass {a, b} {}\) Strict Ordering on Integers is Asymmetric

Then:

\(\ds \eqclass {a, b} {}\) \(>\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\succ\) \(\ds b + c\) Definition of Strict Ordering on Integers
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\ne\) \(\ds b + c\) Definition of Ordering on Natural Numbers
\(\ds \leadsto \ \ \) \(\ds \eqclass {a, b} {}\) \(\ne\) \(\ds \eqclass {c, d} {}\) Definition of Strict Ordering on Integers


and:

\(\ds \eqclass {a, b} {}\) \(=\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds a + d\) \(=\) \(\ds b + c\) Definition of Strict Ordering on Integers
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\nprec\) \(\ds b + c\) Definition of Ordering on Natural Numbers
\(\, \ds \land \, \) \(\ds a + d\) \(\nsucc\) \(\ds b + c\) Definition of Ordering on Natural Numbers
\(\ds \leadsto \ \ \) \(\ds \eqclass {a, b} {}\) \(\nless\) \(\ds \eqclass {c, d} {}\) Definition of Strict Ordering on Integers
\(\, \ds \land \, \) \(\ds \eqclass {a, b} {}\) \(\ngtr\) \(\ds \eqclass {c, d} {}\) Definition of Strict Ordering on Integers

This demonstrates that $<$, $=$ and $>$ are mutually exclusive.


Now:

\(\ds \eqclass {a, b} {}\) \(<\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\prec\) \(\ds b + c\) Definition of Strict Ordering on Integers
\(\ds \leadsto \ \ \) \(\ds b + c\) \(\preccurlyeq\) \(\ds a + d\) Definition of Ordering on Natural Numbers
\(\ds \leadsto \ \ \) \(\ds \eqclass {c, d} {}\) \(\le\) \(\ds \eqclass {a, b} {}\) Definition of Strict Ordering on Integers

Similarly:

\(\ds \eqclass {a, b} {}\) \(>\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\succ\) \(\ds b + c\) Definition of Strict Ordering on Integers
\(\ds \leadsto \ \ \) \(\ds b + c\) \(\succcurlyeq\) \(\ds a + d\) Definition of Ordering on Natural Numbers
\(\ds \leadsto \ \ \) \(\ds \eqclass {c, d} {}\) \(\ge\) \(\ds \eqclass {a, b} {}\) Definition of Strict Ordering on Integers

and:

\(\ds \eqclass {a, b} {}\) \(\ne\) \(\ds \eqclass {c, d} {}\)
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\ne\) \(\ds b + c\) Definition of Strict Ordering on Integers
\(\ds \leadsto \ \ \) \(\ds a + d\) \(\prec\) \(\ds b + c\) Definition of Ordering on Natural Numbers
\(\, \ds \lor \, \) \(\ds a + d\) \(\succ\) \(\ds b + c\) Definition of Ordering on Natural Numbers
\(\ds \leadsto \ \ \) \(\ds \eqclass {a, b} {}\) \(<\) \(\ds \eqclass {c, d} {}\) Definition of Strict Ordering on Integers
\(\, \ds \land \, \) \(\ds \eqclass {a, b} {}\) \(\>\) \(\ds \eqclass {c, d} {}\) Definition of Strict Ordering on Integers

demonstrating that either $<$, $=$ or $>$ must hold.

$\blacksquare$


Sources