Every nonempty subset S of the positive integers has a least element.

Let a and b > 0 be distinct integers.

This is a multi-part proof.

Part 1: prove the existence of q and 0 ≤ r < b such that a = b ⋅ q + r.

r = a - b ⋅ q | | Solve for r. |

Let C = {i | a - b ⋅ i ≥ 0 : a - b ⋅ i} | | Set of possible solutions for r. |

| Prove that the least value for r is the solution for r. | |

a ≥ 0 ⇒ a + 0 = a + b ⋅ 0 ≥ 0 | | Show that set C is non-empty. |

(a + b ⋅ 0) ∈ C | | Criteria for set C satisfied |

C is non-empty | | C has at least 1 member |

Show that 0 ≤ r < b | | |

it suffices to show that r < b | | r ∈ C, 0 ≤ r |

q + 1 > q | | property of numbers |

b ⋅ (q + 1) > b ⋅ q | | multiplying by number > 0 maintains inequality |

b ⋅ q + b > b ⋅ q | | algebra |

- b ⋅ q - b < - b ⋅ q | | Multiplying by -1 changes inequality |

a - b ⋅ q - b < a - b ⋅ q | | adding maintains inequality |

a - b ⋅ q - b < r | | substitution |

a - b ⋅ q b ∉ C | | r is the least element of C, |

| by the well-ordering principle, | |

| any integer less than r is not an element of C: | |

a - b ⋅ q b = a - b ⋅ (q + 1) | | algebra |

a - b ⋅ q b ∈ C ∨ a - b ⋅ q b < 0 | | a - b ⋅ q b has the form of elements of C |

a - b ⋅ q b ∉ C ∧ (a - b ⋅ q b ∈ C ∨ a - b ⋅ q b < 0) |
| combine previous lines |

a - b ⋅ q b ∉ C ∧ (a - b ⋅ q b ∉ C ⇒ a - b ⋅ q b < 0) |
| (p ⇒ q) ≡ (not p ⇒ q) |

a - b ⋅ q b < 0 | | p ∧ (p ⇒ q) ⇒ q (modus ponens) |

r b < 0 | | r = (a - b ⋅ q) |

r < b | | add b doesn't change inequality |

| end of part I |

Part 2: In the equation a = b ⋅ q + r, show that r and q are unique. Suppose that r′ and q′ are two integers such that r′ = a - b ⋅ q′ and 0 ≤ r′ < b. Must show that q = q′.

Suppose that q < q′ ∨ q > q′ | | Assume ¬(q = q′) |

q < q′ ≡ q + 1 ≤ q′ ∧ q > q′ ≡ q 1 ≥ q′ | | q < q + 1 |

q + 1 ≤ q′ ∨ q 1 ≥ q′ | | substitute equivalences in given |

q ≤ q′ - 1 ∨ q ≥ q′ + 1 | | add 1 to both sides preserves the inequality |

| | |

for q ≤ q′ 1: | | |

q ≤ q′ 1 | | given |

b ⋅ q ≤ b ⋅ (q′ 1) | | order preserved, b > 0 |

- b ⋅ q ≥ - b ⋅ (q′ 1) | | negating changes order |

a - b ⋅ q ≥ a - b ⋅ (q′ 1) | | adding preserves order |

a - b ⋅ q ≥ a - b ⋅ q′ + b | | algebra |

r ≥ r′ + b | | substitution |

r ≥ b | | r′ ∈ C ⇒ r′ > 0 |

b > r ≥ b | | 0 < r < b |

false | | order violation |

| | |

for q ≥ q′ + 1 | | |

q ≥ q′ + 1 | | given |

b ⋅ q ≥ b ⋅ (q′ + 1) | | order preserved, b > 0 |

- b ⋅ q ≤ - b ⋅ (q′ + 1) | | negating changes order |

a - b ⋅ q ≤ a - b ⋅ (q′ + 1) | | adding preserves order |

a - b ⋅ q ≤ a - b ⋅ q′ - b | | algebra |

r ≤ r′ - b | | substitution |

r < 0 | | r′ - b < 0 |

0 ≤ r < 0 | | r ∈ C, 0 ≤ r |

false | | order violation |

| | |

q < q′ ∨ q > q′ ⇒ false | | |

q = q′ | | a ≤ b ∨ a = b ∨ a ≥ b |

End of Proof |

**References:**

Long, Calvin T., 1965, Elementary Introduction to Number Theory, Boston, MA: D. C. Heath and Company

Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag