Theorem·T24
The integers are totally ordered
The integer order is a total order: reflexive, antisymmetric, transitive, and any two integers compare.
(D062) is a total order on
.
In words
The integer order is a total order on the integers: reflexive, antisymmetric, transitive, and any two integers compare.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Reflexive. For , unwinds to , which holds since by reflexivity and the equality clause of D029.
- 2Antisymmetric. 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.
- 3Transitive. 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. .
- 4Total. Given , trichotomy compares and in : either (so ) or , hence (so ).
- 5
∎
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.