Skip to content
Axiomatic Wiki

WTThe integers are totally ordered

Theorem·T24

The integer order is a total order: reflexive, antisymmetric, transitive, and any two integers compare.

with from D062 and total order from D052.
In words
The integer order is a total order on the integers: reflexive, antisymmetric, transitive, and any two integers compare.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Reflexive. For , unwinds to , which holds since by reflexivity and the equality clause of D029.
  2. 2
    Antisymmetric. Let and , i.e. and . By trichotomy, exactly one of , , holds. If held, then would force or , and either contradicts trichotomy together with . Symmetrically is impossible. So , which is exactly (L41), giving by T04.
  3. 3
    Transitive. Let , i.e. and . By the gap fact, there are with Adding these and rearranging with commutativity/associativity to expose on both sides: Cancelling : , i.e. , so by the gap fact (witness ), , i.e. .
  4. 4
    Total. Given , trichotomy compares and in : either (so ) or , hence (so ).
  5. 5
    All clauses of D051 hold, plus comparability, so D052 holds: is a totally ordered set.
∎

Remarks

Unlike the naturals (well ordered), has no least element: for any , , so descending chains never terminate. Totality is exactly what the notes there anticipated as the standard example of a total order that is not a well order.
Wikipedia ↗Int.instLinearOrder ↗

Used by

L53T32T35
Propose an edit2 published revisions