Enderton.Set.Chapter_4

Natural Numbers

theorem Enderton.Set.Chapter_4.theorem_4c (n : ℕ) : n = 0 ∨ ∃ (m : ℕ), n = Nat.succ m

Theorem 4C

Every natural number except 0 is the successor of some natural number.

theorem Enderton.Set.Chapter_4.theorem_4i (m : ℕ) (n : ℕ) : m + 0 = m ∧ m + Nat.succ n = Nat.succ (m + n)

Theorem 4I

For natural numbers m and n,

m + 0 = m,
m + n⁺ = (m + n)⁺

theorem Enderton.Set.Chapter_4.theorem_4j (m : ℕ) (n : ℕ) : m * 0 = 0 ∧ m * Nat.succ n = m * n + m

Theorem 4J

For natural numbers m and n,

m ⬝ 0 = 0,
m ⬝ n⁺ = m ⬝ n + m .

theorem Enderton.Set.Chapter_4.left_additive_identity (n : ℕ) : 0 + n = n

Left Additive Identity

For all n ∈ ω, A₀(n) = n. In other words, 0 + n = n.

theorem Enderton.Set.Chapter_4.lemma_2 (m : ℕ) (n : ℕ) : Nat.succ m + n = m + Nat.succ n

Lemma 2

For all m, n ∈ ω, Aₘ₊(n) = Aₘ(n⁺). In other words, m⁺ + n = m + n⁺.

theorem Enderton.Set.Chapter_4.theorem_4k_1 {m : ℕ} {n : ℕ} {p : ℕ} : m + (n + p) = m + n + p

Theorem 4K-1

Associatve law for addition. For m, n, p ∈ ω,

m + (n + p) = (m + n) + p.

theorem Enderton.Set.Chapter_4.theorem_4k_2 {m : ℕ} {n : ℕ} : m + n = n + m

Theorem 4K-2

Commutative law for addition. For m, n ∈ ω,

m + n = n + m.

theorem Enderton.Set.Chapter_4.zero_multiplicand (n : ℕ) : 0 * n = 0

Zero Multiplicand

For all n ∈ ω, M₀(n) = 0. In other words, 0 ⬝ n = 0.

theorem Enderton.Set.Chapter_4.succ_distrib (m : ℕ) (n : ℕ) : Nat.succ m * n = m * n + n

Successor Distribution

For all m, n ∈ ω, Mₘ₊(n) = Mₘ(n) + n. In other words,

m⁺ ⬝ n = m ⬝ n + n.

theorem Enderton.Set.Chapter_4.theorem_4k_3 (m : ℕ) (n : ℕ) (p : ℕ) : m * (n + p) = m * n + m * p

Theorem 4K-3

Distributive law. For m, n, p ∈ ω,

m ⬝ (n + p) = m ⬝ n + m ⬝ p.

theorem Enderton.Set.Chapter_4.succ_identity (m : ℕ) : m + 1 = Nat.succ m

Successor Identity

For all m ∈ ω, Aₘ(1) = m⁺. In other words, m + 1 = m⁺.

theorem Enderton.Set.Chapter_4.right_mul_id (m : ℕ) : m * 1 = m

Right Multiplicative Identity

For all m ∈ ω, Mₘ(1) = m. In other words, m ⬝ 1 = m.

theorem Enderton.Set.Chapter_4.theorem_4k_5 (m : ℕ) (n : ℕ) : m * n = n * m

Theorem 4K-5

Commutative law for multiplication. For m, n ∈ ω, m ⬝ n = n ⬝ m.

theorem Enderton.Set.Chapter_4.theorem_4k_4 (m : ℕ) (n : ℕ) (p : ℕ) : m * (n * p) = m * n * p

Theorem 4K-4

Associative law for multiplication. For m, n, p ∈ ω,

m ⬝ (n ⬝ p) = (m ⬝ n) ⬝ p.

theorem Enderton.Set.Chapter_4.lemma_4l_b (n : ℕ) : ¬n < n

Lemma 4L(b)

No natural number is a member of itself.

theorem Enderton.Set.Chapter_4.zero_least_nat (n : ℕ) : 0 = n ∨ 0 < n

Lemma 10

For every natural number n ≠ 0, 0 ∈ n.

Theorem 4N

For any natural numbers n, m, and p,

m ∈ n ↔ m ⬝ p ∈ n ⬝ p.

If, in addition, p ≠ 0, then

m ∈ n ↔ m ⬝ p ∈ n ⬝ p.

theorem Enderton.Set.Chapter_4.theorem_4n_i (m : ℕ) (n : ℕ) (p : ℕ) : m < n ↔ m + p < n + p

theorem Enderton.Set.Chapter_4.theorem_4n_ii (m : ℕ) (n : ℕ) (p : ℕ) : m < n ↔ m * Nat.succ p < n * Nat.succ p

Corollary 4P

The following cancellation laws hold for m, n, and p in ω:

m + p = n + p ⇒ m = n,
m ⬝ p = n ⬝ p ∧ p ≠ 0 ⇒ m = n.

theorem Enderton.Set.Chapter_4.corollary_4p_i (m : ℕ) (n : ℕ) (p : ℕ) (h : m + p = n + p) : m = n

theorem Enderton.Set.Chapter_4.well_ordering_nat {A : Set ℕ} (hA : Set.Nonempty A) : ∃ m ∈ A, ∀ n ∈ A, m ≤ n

Well Ordering of ω

Let A be a nonempty subset of ω. Then there is some m ∈ A such that m ≤ n for all n ∈ A.

theorem Enderton.Set.Chapter_4.strong_induction_principle_nat (A : Set ℕ) (h : ∀ (n : ℕ), (∀ x < n, x ∈ A) → n ∈ A) : A = Set.univ

Strong Induction Principle for ω

Let A be a subset of ω, and assume that for every n ∈ ω, if every number less than n is in A, then n ∈ A. Then A = ω.

theorem Enderton.Set.Chapter_4.exercise_4_1 : 1 ≠ 3

Exercise 4.1

Show that 1 ≠ 3 i.e., that ∅⁺ ≠ ∅⁺⁺⁺.

theorem Enderton.Set.Chapter_4.exercise_4_13 (m : ℕ) (n : ℕ) (h : m * n = 0) : m = 0 ∨ n = 0

Exercise 4.13

Let m and n be natural numbers such that m ⬝ n = 0. Show that either m = 0 or n = 0.

def Enderton.Set.Chapter_4.even (n : ℕ) : Prop

Call a natural number even if it has the form 2 ⬝ m for some m.

Equations

• Enderton.Set.Chapter_4.even n = ∃ (m : ℕ), 2 * m = n

def Enderton.Set.Chapter_4.odd (n : ℕ) : Prop

Call a natural number odd if it has the form (2 ⬝ p) + 1 for some p.

Equations

• Enderton.Set.Chapter_4.odd n = ∃ (p : ℕ), 2 * p + 1 = n

theorem Enderton.Set.Chapter_4.exercise_4_14 (n : ℕ) : Enderton.Set.Chapter_4.even n ∧ ¬Enderton.Set.Chapter_4.odd n ∨ ¬Enderton.Set.Chapter_4.even n ∧ Enderton.Set.Chapter_4.odd n

Exercise 4.14

Show that each natural number is either even or odd, but never both.

theorem Enderton.Set.Chapter_4.exercise_4_17 (m : ℕ) (n : ℕ) (p : ℕ) : m ^ (n + p) = m ^ n * m ^ p

Exercise 4.17

Prove that mⁿ⁺ᵖ = mⁿ ⬝ mᵖ.

theorem Enderton.Set.Chapter_4.exercise_4_19 (m : ℕ) (d : ℕ) (hd : d ≠ 0) : ∃ (q : ℕ) (r : ℕ), m = d * q + r ∧ r < d

Exercise 4.19

Prove that if m is a natural number and d is a nonzero number, then there exist numbers q and r such that m = (d ⬝ q) + r and r is less than d.

theorem Enderton.Set.Chapter_4.exercise_4_22 (m : ℕ) (p : ℕ) : m < m + Nat.succ p

Exercise 4.22

Show that for any natural numbers m and p we have m ∈ m + p⁺.

theorem Enderton.Set.Chapter_4.exercise_4_23 {m : ℕ} {n : ℕ} (hm : m < n) : ∃ (p : ℕ), m + Nat.succ p = n

Exercise 4.23

Assume that m and n are natural numbers with m less than n. Show that there is some p in ω for which m + p⁺ = n. (It follows from this and the preceding exercise that m is less than n iff (∃p ∈ ω) m + p⁺ = n.)

theorem Enderton.Set.Chapter_4.exercise_4_24 (m : ℕ) (n : ℕ) (p : ℕ) (q : ℕ) (h : m + n = p + q) : m < p ↔ q < n

Exercise 4.24

Assume that m + n = p + q. Show that

m ∈ p ↔ q ∈ n.

theorem Enderton.Set.Chapter_4.exercise_4_25 (m : ℕ) (n : ℕ) (p : ℕ) (q : ℕ) (h₁ : n < m) (h₂ : q < p) : m * q + n * p < m * p + n * q

Exercise 4.25

Assume that n ∈ m and q ∈ p. Show that

(m ⬝ q) + (n ⬝ p) ∈ (m ⬝ p) + (n ⬝ q).