Skip to content
Axiomatic Wiki
Lemma·L47

Order as an additive gap

One number is at most another exactly when some amount added to it reaches the other.

For all :
In words
One natural number is at most another exactly when there is some natural number (possibly zero) that, added to the first, gives the second.
Rests onF02F03F04F06F08F09F11F12F14A01A06A08
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Left to right. Suppose , i.e. or (D029). If , take : by D027. If , L17 (ii) gives with .
  2. 2
    Right to left. Suppose for some . If , D027 gives , so by the equality clause of D029. If , L17 (ii), read right to left, gives , so .
∎

Remarks

The companion to L17 (ii), which is the strict, nonzero-gap version. Used to convert order statements on and on the integer order into additive equations, e.g. in L48 and T24.
Wikipedia ↗Nat.le.dest ↗

Used by

L48T24
Propose an edit1 published revision