nat.n

# Natural numbers: definition

Axiom 1.  There exists a type ℕ with an element 0 ∈ ℕ and a function s : ℕ → ℕ such that

  a. There is no n ∈ ℕ such that s(n) = 0.
  b. For all n, m ∈ ℕ, if s(n) = s(m) then n = m.
  c. Let P : ℕ → 𝔹.  If P(0) is true, and P(k) implies P(s(k)) for all k ∈ ℕ, then P(n) is true for all n ∈ ℕ.

Definition.  Let 1 : ℕ = s(0).

Lemma 1.  Let a ∈ ℕ.  Suppose that a ≠ 0.  Then there is some b ∈ ℕ such that a = s(b).

# Natural numbers: addition

Axiom 2.  There is a binary operation + : ℕ → ℕ → ℕ such that for all n, m ∈ ℕ,

  a. n + 0 = n.
  b. n + s(m) = s(n + m).

Theorem 2.  Let a, b, c ∈ ℕ.

  1. If a + c = b + c, then a = b.
  2. (a + b) + c = a + (b + c).
  3. 0 + a = a = a + 0.
  4. s(a) + b = s(a + b).
  5. a + b = b + a.
  6. a + s(b) ≠ 0.
  7. a + s(b) ≠ a.
  8. If a + b = 0, then a = 0 and b = 0.

# Natural numbers: multiplication

Axiom 3.  There is a binary operation · : ℕ → ℕ → ℕ such that for all n, m ∈ ℕ,

  a. n · 0 = 0.
  b. n · s(m) = (n · m) + n.

Theorem 3.  Let a, b, c ∈ ℕ.

  1. a · 0 = 0 = 0 · a.
  2. a · 1 = a = 1 · a.
  3. c(a + b) = ca + cb.
  4. (ab)c = a(bc). 
  5. s(a) · b = ab + b.
  6. ab = ba.
  7. (a + b)c = ac + bc.

Proof.

  4. Let a, b ∈ ℕ.  Let

        G = { x ∈ ℕ | (a · b) · x = a · (b · x) }.
  
  We have (ab) · 0 = 0 = a(b · 0), so 0 ∈ G.  Now let c ∈ ℕ, and suppose that c ∈ G.  Then

    (a · b) · s(c) = (a · b) · c + a · b      by Axiom 3(b)
                   = a · (b · c) + a · b
                   = a · (b · c + b)                by Theorem 3.3
                   = a · (b · s(c))                  by Axiom 3(b).
                 
  So s(c) ∈ G.  Hence x ∈ G for all x ∈ ℕ.

  5. Let a ∈ ℕ.  Let

        G = { x ∈ ℕ | s(a) · x = ax + x }.
    
  We have s(a) · 0 = 0 = a · 0 + 0, so 0 ∈ G.  Now let b ∈ ℕ, and suppose that b ∈ G.  Then

  s(a) · s(b) = s(a) · b + s(a)
              = (ab + b) + s(a)
              = ab + (b + s(a))
              = ab + s(b + a)
              = ab + s(a + b)
              = ab + (a + s(b))
              = (ab + a) + s(b)
              = a · s(b) + s(b).

  So s(b) ∈ G.  Hence x ∈ G for all x ∈ ℕ.

Theorem 4.  Let a, b ∈ ℕ.

  1. ab = 0 if and only if a = 0 or b = 0.
  2. ab = 1 if and only if a = 1 and b = 1.

# Cancellation of multiplication

Theorem 5.  Let a, b, c ∈ ℕ.  If c ≠ 0 and ac = bc then a = b.

Proof. Let

        G = { x ∈ ℕ | for all y, z ∈ ℕ, if z ≠ 0 and xz = yz then x = y }.

  Let b, c ∈ ℕ with c ≠ 0 and 0 · c = bc. Then bc = 0.  Since c ≠ 0, we must have b = 0 by Theorem 4.1.  So 0 = b, and hence 0 ∈ G.

  Now let a ∈ ℕ, and suppose that a ∈ G.  Let b, c ∈ ℕ, and suppose that c ≠ 0 and s(a) · c = bc.  Then by Theorem 3.5 we deduce that ca + c = bc.  If b = 0, then either s(a) = 0 or c = 0, which is a contradiction.  Hence b ≠ 0.  By Lemma 1 there is some p ∈ ℕ such that b = s(p).  Therefore ca + c = s(p) · c, and we see that ca + c = cp + c.  It follows by Theorem 2.1 that ca = cp, so ac = pc.  By hypothesis it follows that a = p.  Therefore s(a) = s(p) = b.  Hence s(a) ∈ G, and we deduce that x ∈ G for all x ∈ ℕ.

# Natural numbers: inequalities

Definition.  For all a, b ∈ ℕ, a ≤ b iff there is some c ∈ ℕ such that a + c = b.  a < b iff a ≤ b and a ≠ b.

Definition.  For all a, b ∈ ℕ, we write a ≥ b iff b ≤ a.  We write a > b iff b < a.

Theorem 6.  Let a, b, c ∈ ℕ.

  1. a ≤ a, and a ≮ a, and a < s(a).
  2. 0 ≤ a.
  3. If a ≤ b and b ≤ c, then a ≤ c.
  4. If a ≤ b and b < c, then a < c.
  5. If a < b and b ≤ c, then a < c.
  6. If a < b and b < c, then a < c.

Theorem 7.  Let a, b ∈ ℕ.

  1. Precisely one of a < b or a = b or a > b holds.
  2. a ≤ b or b ≤ a.
  3. If a ≤ b and b ≤ a, then a = b.
  4. It cannot be that b < a < b + 1.
  5. a ≤ b if and only if a < b + 1.
  6. a < b if and only if a + 1 ≤ b.

Proof.

  1. Let a, b ∈ ℕ.  Suppose that a < b and a = b.  It then follows that a < a, which is a contradiction to Theorem 6.1.  Now suppose that a = b and a > b.  It follows that a > a, which is similarly a contradiction.  Now suppose that a < b and b < a.  By Theorem 6.6 we deduce that a < a, again a contradiction.

  Now let

      G = { x ∈ ℕ | for all y ∈ ℕ, x < y or x = y or x > y }.

  We will show that x ∈ G for all x ∈ ℕ.  We start by showing that 0 ∈ G.  Let y ∈ ℕ.  By Theorem 6.2 we know that 0 ≤ y.  It follows that y = 0 or y > 0.  Hence 0 ∈ G.

  Now let x ∈ ℕ, and suppose that x ∈ G.  We will show that s(x) ∈ G.  Let y ∈ ℕ.  By hypothesis we know that x < y or x = y or x > y.
  
  First suppose that x < y.  Then there is some p ∈ ℕ such that x + p = y.  If p = 0, then x = y, so s(x) > y by Theorem 6.1.  If p ≠ 0, then by Lemma 1 there is some r ∈ ℕ such that p = s(r), which implies that x + s(r) = y, which implies s(x) + r = y, so s(x) ≤ y, so either s(x) < y or s(x) = y.

  Next suppose that x = y.  Then by Theorem 6.1 it follows that s(x) > x = y.  Finally, suppose that x > y.  We know that s(x) > x, and by Theorem 6.6 it follows that s(x) > y.

  Putting the cases together, we see that s(x) < y or s(x) = y or s(x) > y always holds.  Hence s(x) ∈ G, and we conclude that x ∈ G for all x ∈ ℕ.

# More identities involving inequalities

Theorem 8.  Let a, b, c ∈ ℕ.

  1. a < b if and only if s(a) < s(b).
  2. If a < b then a + c < b + c.
  3. If a + c < b + c then a < b.
  4. If c ≠ 0 and a < b, then ac < bc.
  5. If ac < bc, then a < b.
  
Proof.

  1. Let a, b ∈ ℕ.  Suppose that a < b.  Then there is some c ∈ ℕ such that a + c = b.  So a + 1 + c = b + 1.  Then s(a) + c = s(b), so s(a) < s(b).

  Now suppose that s(a) < s(b).  Then there is some c ∈ ℕ such that s(a) + c = s(b).  So a + 1 + c = b + 1.  Then a + c = b, so a < b.

  2. Let a, b ∈ ℕ.  Suppose that a < b.  Let

      G = { c ∈ ℕ | a + c < b + c }.

  Clearly 0 ∈ G.  Let c ∈ ℕ, and suppose that c ∈ G.  Then a + c < b + c, so s(a + c) < s(b + c) by part (1) of this theorem.  Then a + s(c) < b + s(c), so s(c) ∈ G.  Hence c ∈ G for all c ∈ ℕ.

  3. Let a, b, c ∈ ℕ, and suppose that a + c < b + c.  If a = b then b + c < b + c, a contradiction. If b < a then b + c < a + c by part (2) of this theorem, so b + c < a + c < b + c, also a contradiction.  By Theorem 7.1, the only alternative is a < b.

  5. Let a, b, c ∈ ℕ, and suppose that ac < bc.  If c = 0 then 0 < 0, which is a contradiction.  So c ≠ 0.  If a = b then bc < bc, a contradiction.  If b < a then bc < ac by part (4) of this theorem, so bc < ac < bc, also a contradiction.  By Theorem 7.1, the only alternative is a < b.

Lemma 9.  Let a, b, c, d ∈ ℕ.  If a < b and c < d, then bc + ad < ac + bd.

Proof.

  Let a, b, c, d ∈ ℕ, and suppose that a < b and c < d.  Then there exist g, h ∈ ℕ with g > 0 and h > 0 such that b = a + g and d = c + h.  Then

    ac + bd = ac + (a + g)(c + h)
                = ac + ac + ah + gc + gh
                = ac + gc + ac + ah + gh
                = (a + g)c + a(c + h) + gh
                = (bc + ad) + gh.

   We must have gh > 0, and so ac + bd < bc + ad.

# Integers: definition

Axiom 4.  There exists a type ℤ with a function z : ℕ ⨯ ℕ → ℤ such that

  a. For all a, b, c, d ∈ ℕ, z(a, b) = z(c, d) if and only if a + d = b + c.
  b. For all x ∈ ℤ, there exist some a, b ∈ ℕ such that x = z(a, b).

Definition.  Let 0 : ℤ = z(0, 0).  Let 1 : ℤ = z(1, 0).

Lemma 10.  For all a, b ∈ ℕ, z(a, b) = 0 if and only if a = b.

Lemma 11.  0 : ℤ ≠ 1 : ℤ.

# Integers: addition

Axiom 5.  There is a binary operation + : ℤ → ℤ → ℤ such that for all a, b, c, d ∈ ℕ,

    z(a, b) + z(c, d) = z(a + c, b + d).

Axiom 6.  There is a unary operation − : ℤ → ℤ such that for all a, b ∈ ℕ,

  −z(a, b) = z(b, a).

Theorem 12.  Let i, j, k ∈ ℤ.

  1. (i + j) + k = i + (j + k).
  2. i + j = j + i.
  3. i + 0 = i.
  4. i + (−i) = 0.

Proof.

  1. Let i, j, k ∈ ℤ. We know that there are some a, b, c, d, e, f ∈ ℕ such that i = z(a, b) and j = z(c, d) and k = z(e, f).  Then
  
    (i + j) + k = (z(a, b) + z(c, d)) + z(e, f)
                    = z(a + c, b + d) + z(e, f)
                    = z((a + c) + e, (b + d) + f)
                    = z(a + (c + e), b + (d + f))
                    = z(a, b) + z(c + e, d + f)
                    = z(a, b) + (z(c, d) + z(e, f))
                    = i + (j + k).

  2. Let i, j ∈ ℤ.  There are some a, b, c, d ∈ ℕ such that i = z(a, b) and j = z(c, d).  Then

    i + j = z(a, b) + z(c, d)
          = z(a + c, b + d)
          = z(c + a, d + b)
          = z(c, d) + z(a, b)
          = j + i.

  3. Let i ∈ ℤ.  Then there are some a, b ∈ ℕ such that i = z(a, b).  So

    i + 0 = z(a, b) + z(0, 0)
            = z(a + 0, b + 0)
            = z(a, b)
            = i.

  4. Let i ∈ ℤ.  Then there are some a, b ∈ ℕ such that i = z(a, b).  So

    i + (−i) = z(a, b) + −z(a, b)
                = z(a, b) + z(b, a)
                = z(a + b, b + a)
                = z(0, 0)     by Axiom 4(a)
                = 0.

Theorem 13.  Let x, y, z ∈ ℤ.

  1. If x + z = y + z, then x = y.
  2. −(−x) = x.
  3. −(x + y) = (−x) + (−y).

# Integers: multiplication

Axiom 7.  There is a binary operation · : ℤ → ℤ → ℤ such that for all a, b, c, d ∈ ℕ,

    z(a, b) · z(c, d) = z(ac + bd, ad + bc).

Theorem 14.  Let i, j, k ∈ ℤ.

  1. (ij)k = i(jk).
  2. ij = ji.
  3. i · 1 = i.
  4. i(j + k) = ij + ik.
  
Proof.

  1. Let i, j, k ∈ ℤ.  There are some a, b, c, d, e, f ∈ ℕ such that i = z(a, b) and j = z(c, d) and k = z(e, f).  Then

    (ij)k = (z(a, b) · z(c, d)) · z(e, f)
          = z(ac + bd, ad + bc) · z(e, f)
          = z((ac + bd)e + (ad + bc)f, (ac + bd)f + (ad + bc)e)
          = z(ace + bde + adf + bcf, acf + bdf + ade + bce)
          = z(ace + adf + bcf + bde, acf + ade + bce + bdf)
          = z(a(ce + df) + b(cf + de), a(cf + de) + b(ce + df))
          = z(a, b) · z(ce + df, cf + de)
          = z(a, b) · (z(c, d) · z(e, f))
          = i(jk).

  2. Let i, j ∈ ℤ.  Then there are some a, b, c, d ∈ ℕ such that i = z(a, b) and j = z(c, d).  Then

    ij = z(a, b) · z(c, d)
      = z(ac + bd, ad + bc)
      = z(ca + db, cb + da)
      = z(c, d) · z(a, b)
      = ji.

  4. Let i, j, k ∈ ℤ.  There are some a, b, c, d, e, f ∈ ℕ such that i = z(a, b) and j = z(c, d) and k = z(e, f).  Then

    i(j + k) = z(a, b) · (z(c, d) + z(e, f))
                = z(a, b) · z(c + e, d + f)
                = z(a(c + e) + b(d + f), a(d + f) + b(c + e))
                = z(ac + ae + bd + bf, ad + af + bc + be)
                = z(ac + bd + ae + bf, ad + bc + af + be)
                = z(ac + bd, ad + bc) + z(ae + bf, af + be)
                = z(a, b) · z(c, d) + z(a, b) · z(e, f)
                = ij + ik.

Theorem 15.  Let i, j ∈ ℤ.  If ij = 0, then i = 0 or j = 0.

Proof.

  Let i, j ∈ ℤ.  Suppose that ij = 0 and that i ≠ 0.  We will deduce that j = 0.  There are some a, b, c, d ∈ ℕ such that i = z(a, b) and j = z(c, d).  So by Axiom 7 we see that ij = z(ac + bd, ad + bc).  It then follows from Lemma 8 that a ≠ b and ac + bd = ad + bc.  By Theorem 7.1 we know that either a < b or a > b.
  
  First, suppose that a < b.  Then there is some g ∈ ℕ such that a + g = b.  Hence ac + (a + g)d = ad + (a + g)c.  So ac + ad + gd = ad + ac + gc, so gd = gc.  Since a ≠ b, we must have g ≠ 0, and we deduce that d = c.

  Next, suppose that a > b.  Then there is some g ∈ ℕ such that b + g = a.  Hence (b + g)c + bd = (b + g)d + bc.  So bc + gc + bd = bd + gd + bc, so gc = gd.  Since a ≠ b, we must have g ≠ 0, and we deduce that c = d.  

  In either case c = d.  Then j = 0 by Lemma 8.

Theorem 16.  Let i, j, k ∈ ℤ.

  1. i · 0 = 0.
  2. If k ≠ 0 and ik = jk, then i = j.
  3. (−i)j = −(ij) = i(−j).
  4. ij = 1 if and only if i = j = 1 or i = j = −1.

# Integers: inequalities

Axiom 8.  There is a relation < : ℤ → ℤ → 𝔹 such that for all a, b, c, d ∈ ℕ,

    z(a, b) < z(c, d) if and only if a + d < b + c.

Definition.  For all i, j ∈ ℤ, we write i > j iff j < i.

Theorem 17.  Let i, j, k ∈ ℤ.

  1. Precisely one of i < j or i = j or i > j holds.
  2. If i < j and j < k, then i < k.
  3. If i < j then i + k < j + k.
  4. If i < j and k > 0, then ik < jk.

Proof.

  1. Let i, j ∈ ℤ.  Then there are some a, b, c, d ∈ ℕ such that i = z(a, b) and j = z(c, d).  By Theorem 7.1 we know that exactly one of a + d < b + c or a + d = b + c or a + d > b + c holds.  The result follows using Axiom 8.

  2. Let i, j, k ∈ ℤ, and suppose that i < j and j < k.  There are some a, b, c, d, e, f ∈ ℕ such that i = z(a, b) and j = z(c, d) and k = z(e, f).  Then z(a, b) < z(c, d) and z(c, d) < z(e, f), so a + d < b + c and c + f < d + e.  It follows that a + d + f < b + c + f and b + c + f < b + d + e, so a + d + f < b + d + e.  Then a + f < b + e by Theorem 8.3, so i < k.

  3. Let i, j, k ∈ ℤ, and suppose that i < j.  There are some a, b, c, d, e, f ∈ ℕ such that i = z(a, b) and j = z(c, d) and k = z(e, f).  Then z(a, b) < z(c, d), and therefore a + d < b + c.  Hence (a + d) + (e + f) < (b + c) + (e + f), and therefore (a + e) + (d + f) < (b + f) + (c + e).  It follows by Axiom 8 that z(a + e, b + f) < z(c + e, d + f), and hence z(a, b) + z(e, f) < z(c, d) + z(e, f), which means that i + k < j + k.

  4. Let i, j, k ∈ ℤ, and suppose that i < j and k > 0.  There are some a, b, c, d, e, f ∈ ℕ such that i = z(a, b) and j = z(c, d) and k = z(e, f). So z(a, b) < z(c, d) and z(e, f) > 0, which means that a + d < b + c and f < e.  So by Lemma 8 we have
  
    (b + c)f + (a + d)e < (a + d)f + (b + c)e.

  Then
  
    (ae + bf) + (cf + de) < (af + be) + (ce + df).
    
  So z(ae + bf, af + be) < z(ce + df, cf + de) by Axiom 8.  And so z(a, b) · z(e, f) < z(c, d) · z(e, f), so we have ik < jk.