Theorem·T10
The division algorithm
Dividing with remainder: quotient and remainder exist and are unique.
For all
with
, there exist unique
such that
is the quotient and
the remainder of
divided by
. Addition from D027, multiplication from D028, order from D029.
In words
For any natural numbers a and b with b non-zero, there is exactly one pair of natural numbers q and r such that a equals q times b plus r and r is strictly below b: q is the quotient and r the remainder of a divided by b.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Existence, by induction on (T05 on , Separation; fixed throughout).
- 2
- 3
- 4Case : the pair witnesses directly.
- 5
- 6Uniqueness of the quotient: suppose with and , and suppose ; by L16 assume (the other case is symmetric). L17 (ii) gives with , and L15 (vii) writes . Then by distributivity (mirrored via L12) and Claim B of L11. So using associativity, and cancellation leaves .
- 7Rearranging with commutativity and associativity, , so by L17 (i). But , and chaining gives (L15 (ii), equality case by substitutivity), contradicting irreflexivity (L15 (i), negation). Hence .
- 8Uniqueness of the remainder: with , the equation reads , and cancellation gives .
∎
Remarks
Euclidean division, the fundamental computation of arithmetic. Everything algorithmic about the integers flows from it: decimal notation (divide by ten, keep the remainder), the Euclidean algorithm for greatest common divisors, and modular arithmetic (
and
are congruent mod
when they leave the same remainder). The existence half is a single induction; the uniqueness half is where the order theory of L17 and L18 earns its keep. Note the theorem does not need well-ordering, though the textbook proof via "least
" uses it; on
, plain induction suffices.