Skip to content
Axiomatic Wiki
Lemma·L16

Trichotomy

Any two naturals compare: less, equal, or greater, and only one.

For all , exactly one of holds, with from D029.
In words
Given two natural numbers m and n, exactly one of three things happens: m is smaller than n, m and n are equal, or n is smaller than m.
Rests onF02F03F04F06F09F11F12F14A01A06A08
Never needed: F05 · F08 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    At most one. If and , then , contradicting L15 (i) via substitutivity. If and , then and , a two-cycle forbidden by L05 (ii). If and , then , again contradicting L15 (i) via substitutivity. (Negation of each conjunction.)
  2. 2
    At least one. Let (Separation); we show by T05.
  3. 3
    Base: for any , L15 (iv) gives , i.e. or ; flipping the equality with symmetry yields or , so the disjunction at holds.
  4. 4
    Step: let and . By hypothesis: , or , or . If : then by L15 (ii) and (vi). If : then by (vi). If : then by (v), i.e. or (symmetry gives ). In every case one of , , holds, so .
  5. 5
    T05 concludes , and with step 1 the three cases are mutually exclusive.
∎

Remarks

Trichotomy says the order on is total: no two naturals are incomparable. Together with L15 it makes a strict total order, and with well-ordering the prototype of an ordinal. Downstream it is the tool for turning "not less" into "greater or equal", used in the division algorithm, Euclid's theorem and dozens of places silently.
Wikipedia ↗Nat.lt_trichotomy ↗

Used by

L17L18L19L20L23L26L33L35T09T10T11T18T19T24T32T35
Propose an edit1 published revision