Skip to content
Axiomatic Wiki

WLSign normal form of an integer

Lemma·L75

Every integer is the image of a natural number or the negative of the image of a positive one.

For every , exactly one of holds, with from D057 and from D059.
In words
Every integer is either the image of a natural number or the negative of the image of a positive natural number, and never both.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Write with (D056). By trichotomy on , either or .
  2. 2
    Case . By L47 there is with . Then because (commutativity, L41), so (D057): the first form.
  3. 3
    Case . By L17 (ii) there is with and . Then because (D027, L41), so (as , D059): the second form.
  4. 4
    Exclusivity. If both forms held, then with , so , that is (L46, with ). Injectivity (L42) gives . But means , whence (D027, T06 (P3)), a contradiction. So exactly one form holds.
∎

Remarks

The sign trichotomy of : the image of is exactly the nonnegative integers, and everything else is strictly negative. Through D062, holds exactly when for some . This normal form is the standard device for reducing an integer statement to a natural-number one by two cases; it is used in L76, L77, and wherever a nonnegative integer must be named as of a natural.
Wikipedia ↗Int.eq_nat_or_neg ↗

Used by

L76L77
Propose an edit1 published revision