Skip to content
Axiomatic Wiki
Lemma·L17

Order and addition

Less-than means a non-zero gap; adding preserves comparisons.

For all , with and from D029 and from D027:(i) ;(ii) ;(iii) .
In words
A number never exceeds itself plus something; being strictly smaller means differing by a non-zero amount; and adding the same number to both sides neither creates nor destroys a strict comparison.
Rests onF02F03F04F06F08F09F11F12F14A01A06A08
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    (i) Induction on (T05, Separation). Base: (D027) and . Step: if , then since by L15 (vi) and D027, either or with L15 (ii); both give .
  2. 2
    (ii), right to left: let with . By L15 (vii), for some , so (D027). By (i), , and by L15 (vi); combining (L15 (ii) in the strict case) gives .
  3. 3
    (ii), left to right: induction on with quantified inside: . Base: is impossible (D002), so . Step: let ; by L15 (iii), . If : take ; then (D027), and by (P3). If : the hypothesis gives with ; then and by (P3). So , and T05 finishes.
  4. 4
    (iii), left to right: if , take with (by (ii)). Then by associativity and commutativity, and , so by (ii) right to left.
  5. 5
    (iii), right to left: suppose . By L16, compare and : if then , contradicting L15 (i); if then by the direction just proved, and with this is a two-cycle in , contradicting L16 (at most one). So .
∎

Remarks

Part (ii) is the naturals' substitute for subtraction: "the gap exists as a number". It converts order statements into equations, which is how the division algorithm, multiplicative monotonicity and the counting lemmas (L26) manipulate inequalities without ever leaving .
Wikipedia ↗Nat.add_lt_add_iff_right ↗

Used by

L18L19L26L33L35L47L51L64T10T11T29
Propose an edit2 published revisions