Skip to content
Axiomatic Wiki
Lemma·L42

The embedding of the naturals is injective

Distinct natural numbers give distinct integers.

(D057) is injective: for , if then .
In words
For any natural numbers m and n, if m and n give the same integer under the embedding, they were already the same natural number.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Suppose , i.e. . By T04 applied to ∼, this holds exactly when , i.e. .
  2. 2
    By D027, and , so .
∎

Remarks

Together with L46 and L49, this makes an order-preserving injective homomorphism: a faithful copy of sitting inside .
Wikipedia ↗Int.ofNat.inj ↗

Used by

T27
Propose an edit1 published revision