Whole-number arithmetic

Neema helps on her family's farm near Arusha, in Tanzania. One morning the hens have laid 347 eggs. The eggs go to market in trays, and each tray holds 30 eggs.

• How many trays can Neema fill?
• How many eggs will be left over?
• Next week the farm sells 23 full trays. How many eggs is that?

The first two questions are about dividing, the last one about multiplying. You already know how to add and subtract using tens and ones (addition, subtraction and place value). You may also know methods for multiplying and dividing. In this lesson we find out why those methods work, so that you never have to trust a rule you don't understand.

Multiplication counts equal groups. Four trays with $6$ eggs in each hold $4 \times 6 = 6 + 6 + 6 + 6 = 24$ eggs.

We can also set things out in rows and columns, as an array. An array with $4$ rows of $6$ has $4 \times 6$ objects. Now turn the array on its side: it becomes $6$ rows of $4$. Nothing was added and nothing was taken away, so

That works for any array. Turning it never changes how many things are in it.

Multiplication obeys three laws. They are true for all whole numbers $a$, $b$ and $c$:

Two more facts complete the toolkit: $a \times 1 = a$ and $a \times 0 = 0$.

Division often does not come out exactly. When it doesn't, something is left over.

The condition $r < b$ matters. If $r$ were $b$ or more, we could make one more full group!

The distributive law as a picture. A rectangle $7$ squares tall and $6 + 4$ squares wide can be cut into two rectangles. Press "Pull the parts apart" and change the sliders:

Notice that $7 \times (6 + 4) = 7 \times 6 + 7 \times 4$, whatever numbers you choose.

Division with remainder as an array. Arrange $23$ dots in rows of $5$. You get $4$ full rows and $3$ dots left over: $23 = 4 \times 5 + 3$. Try other row lengths. When are there no dots left over?

Why the laws are true

• Commutative: turn the array (see above).
• Associative: build a box of cubes, $a$ long, $b$ wide and $c$ tall. Count it as $c$ layers of $a \times b$ cubes, or as $a$ slices of $b \times c$ cubes. Either way it is the same box, so $(a \times b) \times c = a \times (b \times c)$.
• Distributive: a rectangle $a$ tall and $b + c$ wide splits into one $a$ by $b$ rectangle and one $a$ by $c$ rectangle, as in the explorer.

Why the written multiplication method works

Let us multiply $23 \times 47$. Place value says $23 = 20 + 3$ and $47 = 40 + 7$. Draw a rectangle $23$ tall and $47$ wide, and cut it along those lines:

The distributive law, used twice, says exactly this:

The column method adds the same four pieces, grouped into rows:

      4 7
    × 2 3
    -----
    1 4 1     ← 47 × 3  = 3 × 40 + 3 × 7  = 120 + 21
    9 4 0     ← 47 × 20 = 20 × 40 + 20 × 7 = 800 + 140
    -----
  1 0 8 1

In the first row, $7 \times 3 = 21$ ones. We write $1$ in the ones column and carry the $2$. Carrying is not a trick. Twenty ones are two tens, so we move them to the tens column. Then $4 \times 3 = 12$ tens, plus the $2$ carried tens, makes $14$ tens: $4$ tens and $1$ hundred. The second row starts with a $0$ because we are multiplying by $2$ tens: $47 \times 20 = 47 \times 2 \times 10$.

Why long division works

Long division shares out one place value at a time. Here is $953 \div 4$, sharing $953$ among $4$ people:

1. Hundreds. $9$ hundreds shared by $4$ is $2$ hundreds each, using $8$. $1$ hundred is left.
2. Trade the leftover hundred for $10$ tens. With the $5$ tens we had, that makes $15$ tens. Each person gets $3$ tens, using $12$. $3$ tens are left.
3. Trade those $3$ tens for $30$ ones. With the $3$ ones, that makes $33$ ones. Each person gets $8$, using $32$. $1$ is left.

Each person got $2$ hundreds, $3$ tens and $8$ ones, so

Why there is only one quotient and one remainder

Why we cannot divide by zero

"$6 \div 2 = 3$" is a short way to say "$3$ is the number with $3 \times 2 = 6$". So what would $5 \div 0$ be? It would be a number $q$ with $q \times 0 = 5$. But $q \times 0 = 0$ for every number $q$. No number works, so $5 \div 0$ has no answer.

And $0 \div 0$? Now every number works, because $q \times 0 = 0$ is always true. A division that has every number as its answer tells us nothing, so $0 \div 0$ has no answer either. That is why we say division by zero is undefined. (Division with remainder also needs $b > 0$: no remainder $r$ could be smaller than $0$.)

1. "$7 \times 98 = 686$." — True. $7 \times 100 - 7 \times 2 = 700 - 14 = 686$.
2. "For every whole number $n$, $n \times 1 = n$." — True. $n$ groups of $1$ make $n$.
3. "Multiplying always makes a number bigger." — False! $9 \times 1 = 9$, which is not bigger than $9$. One counterexample is enough to show that an "always" statement is false.
4. "$23 \div 5$ is $3$ remainder $8$." — False. $23 = 3 \times 5 + 8$ is a true equation, but the rule says the remainder must be less than $5$. Being precise about the rule matters.
5. "Some number times $0$ is $5$." — False. Every number times $0$ is $0$.

/-- `a × 98 = a × 100 − a × 2` for every whole number `a`: since `100 = 98 + 2`, the
distributive law gives `a × 100 = a × 98 + a × 2`, and taking away `a × 2` leaves `a × 98`.
So `7 × 98 = 700 − 14 = 686`. -/
theorem times_ninety_eight (a : Nat) : a * 98 = a * 100 - a * 2 := by
  have h : a * 100 = a * 98 + a * 2 :=
    calc a * 100 = a * (98 + 2) := rfl
      _ = a * 98 + a * 2 := Nat.mul_add a 98 2
  rw [h, Nat.add_sub_cancel]

/-- The worked example: `7 × 98 = 7 × 100 − 7 × 2 = 686`. Lean evaluates both sides. -/
theorem seven_times_ninety_eight : 7 * 98 = 7 * 100 - 7 * 2 ∧ 7 * 98 = 686 := by decide

/-- `25 × 36 = 900`, by regrouping: `36 = 4 × 9`, and the associative law lets us multiply
`25 × 4 = 100` first. Each line of the `calc` block is one step of the mental calculation. -/
theorem twenty_five_times_thirty_six : 25 * 36 = 900 :=
  calc 25 * 36 = 25 * (4 * 9) := rfl
    _ = (25 * 4) * 9 := (Nat.mul_assoc 25 4 9).symm
    _ = 100 * 9 := rfl
    _ = 900 := rfl

/-- The distributive law `a × (b + c) = a × b + a × c`. This applies core Lean's
theorem `Nat.mul_add`. -/
theorem distrib_library (a b c : Nat) : a * (b + c) = a * b + a * c := Nat.mul_add a b c

/-- `0 × a = 0`: any number of copies of `0` add up to `0`. Proved by induction on `a`, using
only Lean's definition `n * (m + 1) = n * m + n`. -/
theorem zero_mul_from_definition (a : Nat) : 0 * a = 0 := by
  induction a with
  | zero => rfl
  | succ n ih => rw [Nat.mul_succ, ih]

/-- `(a + 1) × b = a × b + b`: making every one of the `b` copies one bigger adds `b` in all.
Proved by induction on `b` from the definition of multiplication. -/
theorem succ_mul_from_definition (a b : Nat) : (a + 1) * b = a * b + b := by
  induction b with
  | zero => rfl
  | succ n ih =>
    calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) := Nat.mul_succ (a + 1) n
      _ = a * n + n + (a + 1) := by rw [ih]
      _ = (a * n + a) + (n + 1) := by omega
      _ = a * (n + 1) + (n + 1) := by rw [Nat.mul_succ]

/-- The commutative law `a × b = b × a`, proved from the definition of multiplication as
repeated addition (by induction on `b`, with the two lemmas above). Lean's `a * b` means
"`b` copies of `a`", the opposite reading from "`a` groups of `b`"; this theorem is exactly why
the choice does not matter. -/
theorem mul_comm_from_definition (a b : Nat) : a * b = b * a := by
  induction b with
  | zero => rw [Nat.mul_zero, zero_mul_from_definition]
  | succ n ih => rw [Nat.mul_succ, ih, succ_mul_from_definition]

/-- The commutative law again, this time by applying core Lean's theorem `Nat.mul_comm`. -/
theorem mul_comm_library (a b : Nat) : a * b = b * a := Nat.mul_comm a b

/-- The area model: `(a + b) × (c + d)` is the sum of the four partial products. Split the
first factor (distributive law on the right), then split each part again (on the left). -/
theorem area_model (a b c d : Nat) :
    (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
  calc (a + b) * (c + d) = a * (c + d) + b * (c + d) := Nat.add_mul a b (c + d)
    _ = (a * c + a * d) + (b * c + b * d) := by rw [Nat.mul_add a c d, Nat.mul_add b c d]
    _ = a * c + a * d + b * c + b * d := (Nat.add_assoc (a * c + a * d) (b * c) (b * d)).symm

/-- `23 × 47 = 1081`, as four partial products: `20 × 40 + 20 × 7 + 3 × 40 + 3 × 7`
`= 800 + 140 + 120 + 21`. The first step is `area_model` with `23 = 20 + 3` and `47 = 40 + 7`. -/
theorem twenty_three_times_forty_seven :
    23 * 47 = 20 * 40 + 20 * 7 + 3 * 40 + 3 * 7 ∧ 23 * 47 = 1081 :=
  ⟨area_model 20 3 40 7, rfl⟩

/-- 347 eggs fill 11 trays of 30, with 17 eggs left over: `347 = 11 × 30 + 17` and `17 < 30`.
Lean's `/` and `%` compute the same quotient and remainder. -/
theorem eggs_in_trays : 347 = 11 * 30 + 17 ∧ 17 < 30 ∧ 347 / 30 = 11 ∧ 347 % 30 = 17 := by
  decide

/-- Division with remainder always works: for `b > 0`, every `a` can be written as
`a = q × b + r` with `r < b`. The proof adds eggs one at a time (induction on `a`). Each new
egg either goes into the unfinished tray, or it completes that tray and the leftover pile
starts again at `0`. -/
theorem div_mod_exists (a b : Nat) (hb : 0 < b) : ∃ q r, a = q * b + r ∧ r < b := by
  induction a with
  | zero => exact ⟨0, 0, by rw [Nat.zero_mul], hb⟩
  | succ n ih =>
    obtain ⟨q, r, h, _hr⟩ := ih
    by_cases hfit : r + 1 < b
    · -- The new egg fits in the unfinished tray: the remainder grows by one.
      exact ⟨q, r + 1, by omega, hfit⟩
    · -- The new egg completes the tray (`r + 1 = b`): one more full tray, nothing left over.
      have hrb : r + 1 = b := by omega
      refine ⟨q + 1, 0, ?_, hb⟩
      calc n + 1 = q * b + (r + 1) := by omega
        _ = q * b + b := by rw [hrb]
        _ = (q + 1) * b + 0 := by rw [Nat.succ_mul, Nat.add_zero]

/-- The quotient and remainder are unique. If `q × b + r = q' × b + r'` with both remainders
less than `b`, then `q = q'` and `r = r'`. If `q` were smaller than `q'`, the right side
would be at least `(q + 1) × b = q × b + b`, which is more than `q × b + r`. -/
theorem div_mod_unique {b q r q' r' : Nat} (h : q * b + r = q' * b + r')
    (hr : r < b) (hr' : r' < b) : q = q' ∧ r = r' := by
  have hq : q = q' := by
    rcases Nat.lt_trichotomy q q' with hlt | heq | hgt
    · have hle : (q + 1) * b ≤ q' * b := Nat.mul_le_mul_right b hlt
      rw [Nat.succ_mul] at hle
      omega
    · exact heq
    · have hle : (q' + 1) * b ≤ q * b := Nat.mul_le_mul_right b hgt
      rw [Nat.succ_mul] at hle
      omega
  subst hq
  exact ⟨rfl, by omega⟩

/-- Lean's own quotient `a / b` and remainder `a % b` satisfy `a = (a / b) × b + a % b` with
`a % b < b`. This applies the core theorems `Nat.div_add_mod'` and `Nat.mod_lt`. -/
theorem div_mod_library (a b : Nat) (hb : 0 < b) : a = a / b * b + a % b ∧ a % b < b :=
  ⟨(Nat.div_add_mod' a b).symm, Nat.mod_lt a hb⟩

/-- The long division in the lesson: `953 ÷ 4` is `238` remainder `1`. -/
theorem long_division_953 : 953 = 238 * 4 + 1 ∧ 1 < 4 := by decide

/-- There is no answer to `5 ÷ 0`: no number `q` has `q × 0 = 5`, because `q × 0 = 0`. -/
theorem no_division_by_zero : ¬ ∃ q : Nat, q * 0 = 5 := by
  intro ⟨q, hq⟩
  rw [Nat.mul_zero] at hq
  -- `hq : 0 = 5`, which is false.
  exact absurd hq (by decide)

/-- And `0 ÷ 0` has no single answer: *every* `q` satisfies `q × 0 = 0`.
This applies core Lean's `Nat.mul_zero`. -/
theorem zero_div_zero_every (q : Nat) : q * 0 = 0 := Nat.mul_zero q

/-- "Multiplying always makes a number bigger" is false. One counterexample is enough:
`9 × 1 = 9` is not bigger than `9`. -/
theorem multiplying_need_not_enlarge : ¬ ∀ a b : Nat, a < a * b := by
  intro h
  have h91 : 9 < 9 * 1 := h 9 1
  exact absurd h91 (by decide)

"""The written multiplication method, step by step, checked against Python.

The column method multiplies by one digit at a time, regrouping ("carrying")
ten ones as one ten, then adds the partial products shifted by place value.
The area model splits both numbers by place value and adds the same partial
products in a different grouping. We print the working for 47 x 23, compare
the digit-by-digit method with Python's built-in multiplication on every pair
of numbers below 200 and on random large pairs, and show what goes wrong when
the carries are forgotten.
"""

import random

def digits(n):
    """Digits of a whole number, ones first: digits(407) == [7, 0, 4]."""
    if n < 0:
        raise ValueError("whole numbers only")
    out = [n % 10]
    n //= 10
    while n:
        out.append(n % 10)
        n //= 10
    return out

def from_digits(ds):
    """Inverse of digits(): from_digits([7, 0, 4]) == 407."""
    return sum(d * 10 ** k for k, d in enumerate(ds))

def times_one_digit(a, d, carry_on=True):
    """Multiply a by a single digit d as in the column method.

    Returns (product, steps) where each step is (digit, digit*d + carry_in,
    written digit, carry_out). With carry_on=False the carries are dropped,
    which is the classic mistake.
    """
    if not 0 <= d <= 9:
        raise ValueError("d must be a single digit")
    carry, written, steps = 0, [], []
    for x in digits(a):
        total = x * d + carry
        new_carry = total // 10 if carry_on else 0
        written.append(total % 10)
        steps.append((x, total, total % 10, new_carry))
        carry = new_carry
    while carry:
        written.append(carry % 10)
        carry //= 10
    return from_digits(written), steps

def partial_products(a, b, carry_on=True):
    """The rows of the column method: a times each digit of b, shifted."""
    return [times_one_digit(a, d, carry_on)[0] * 10 ** k
            for k, d in enumerate(digits(b))]

def column_multiply(a, b, carry_on=True):
    """Multiply by the written column method."""
    return sum(partial_products(a, b, carry_on))

def area_pieces(a, b):
    """Area model: each non-zero place-value part of a times each part of b."""
    def parts(n):
        return [d * 10 ** k for k, d in enumerate(digits(n)) if d]
    return [(x, y, x * y) for x in parts(a)[::-1] for y in parts(b)[::-1]]

def count_mismatches(pairs, carry_on=True):
    """How many pairs (a, b) the column method gets wrong."""
    return sum(column_multiply(a, b, carry_on) != a * b for a, b in pairs)

def main():
    a, b = 47, 23
    print(f"Column method for {a} x {b}")
    product, steps = times_one_digit(a, 3)
    for x, total, write, carry in steps:
        print(f"  {x} x 3 + carry = {total}: write {write}, carry {carry}")
    rows = partial_products(a, b)
    print(f"  row 1: {a} x 3 = {rows[0]}")
    print(f"  row 2: {a} x 20 = {a} x 2 x 10 = {rows[1]}")
    print(f"  total: {rows[0]} + {rows[1]} = {sum(rows)}")
    pieces = area_pieces(a, b)
    print("Area model: " + ", ".join(f"{x} x {y} = {p}" for x, y, p in pieces))
    print("  " + " + ".join(str(p) for _, _, p in pieces)
          + f" = {sum(p for _, _, p in pieces)} (same pieces, regrouped)")
    print()
    small = [(x, y) for x in range(200) for y in range(200)]
    rng = random.Random(2024)
    big = [(rng.randrange(10 ** 5, 10 ** 6), rng.randrange(10 ** 3, 10 ** 4))
           for _ in range(2000)]
    print("Column method versus Python's built-in multiplication:")
    print(f"  all {len(small):,} pairs below 200: "
          f"{count_mismatches(small)} mismatches")
    print(f"  {len(big):,} random 6-digit x 4-digit pairs: "
          f"{count_mismatches(big)} mismatches")
    wrong = count_mismatches(small, carry_on=False)
    print("A broken method that forgets to carry:")
    print(f"  47 x 3 gives {column_multiply(47, 3, carry_on=False)}, not 141;"
          f" wrong on {wrong:,} of the {len(small):,} pairs")
    print()
    print("Epistemic status: the 40,000 small pairs are checked completely, so the")
    print("method is correct for those; the random pairs are evidence only. Why it")
    print("works for every pair is the lesson's argument: place value plus the")
    print("distributive law.")

if __name__ == "__main__":
    main()

Checking all $40{,}000$ pairs below $200$ is a complete check of those pairs, but there are infinitely many pairs of numbers. The area-model argument covers them all.

"""Division with remainder: one quotient and one remainder, found by search.

For a = q x b + r there are many pairs (q, r) if r may be as large as we like,
but exactly one with 0 <= r < b. We find the answer for 347 eggs in trays of 30
by repeated subtraction, list every pair that would work without the rule
r < b, and then search exhaustively: for every a up to 500 and b from 1 to 12
there is exactly one pair with r < b, and it agrees with Python's divmod.
Finally we see that "5 divided by 0" has no candidate answer at all.
"""

def repeated_subtraction(a, b):
    """Take b away from a as often as possible; return (quotient, remainder)."""
    if b <= 0:
        raise ValueError("b must be positive")
    if a < 0:
        raise ValueError("a must be a whole number")
    q = 0
    while a >= b:
        a -= b
        q += 1
    return q, a

def all_pairs(a, b, small_remainder=True):
    """Every (q, r) of whole numbers with q*b + r == a (and r < b if asked)."""
    if b <= 0:
        raise ValueError("b must be positive")
    pairs = []
    for q in range(a // b + 1):
        r = a - q * b
        if r >= 0 and (r < b or not small_remainder):
            pairs.append((q, r))
    return pairs

def exhaustive_check(max_a, max_b):
    """Return (cases, all unique?, all agree with divmod?)."""
    cases, unique, agree = 0, True, True
    for a in range(max_a + 1):
        for b in range(1, max_b + 1):
            cases += 1
            pairs = all_pairs(a, b)
            unique = unique and len(pairs) == 1
            agree = agree and pairs == [divmod(a, b)]
    return cases, unique, agree

def solutions_of_times_zero(target, search_up_to):
    """All q in 0..search_up_to with q * 0 == target."""
    return [q for q in range(search_up_to + 1) if q * 0 == target]

def main():
    q, r = repeated_subtraction(347, 30)
    print(f"347 eggs, trays of 30: take away 30 a total of {q} times,"
          f" {r} eggs left.")
    print(f"  347 = {q} x 30 + {r}, and {r} < 30")
    loose = all_pairs(347, 30, small_remainder=False)
    shown = ", ".join(f"({a}, {b})" for a, b in loose[:4])
    print(f"Without the rule r < 30 there are {len(loose)} pairs (q, r):")
    print(f"  {shown}, ..., {loose[-1]}")
    print(f"With the rule r < 30 there is only {all_pairs(347, 30)}")
    print()
    cases, unique, agree = exhaustive_check(500, 12)
    print(f"Every a from 0 to 500 and b from 1 to 12 ({cases:,} cases):")
    print(f"  exactly one pair with r < b every time: {unique}")
    print(f"  that pair is Python's divmod(a, b) every time: {agree}")
    print()
    print("Dividing by zero: q x 0 = 5 for q in 0..1000? "
          f"{len(solutions_of_times_zero(5, 1000))} solutions.")
    print("  q x 0 = 0 for q in 0..1000? "
          f"{len(solutions_of_times_zero(0, 1000))} solutions: every q works.")
    print()
    print("Epistemic status: the search is complete for the 6,012 cases it")
    print("checks, so uniqueness is certain there and nowhere else. The lesson's")
    print("argument (multiples of b are b apart) proves it for every a and b > 0.")
    print("The zero search is evidence; q x 0 = 0 for every q is the proof.")

if __name__ == "__main__":
    main()

Take your time. You can open a hint whenever you like.

What time will it be $29$ hours from now? Remainders can answer that, and they lead to a whole new kind of arithmetic. This trail is optional.

In the sets lesson you met the Cartesian product $A \times B$, the set of all pairs $(a, b)$. If Juma has $3$ shirts and $4$ pairs of trousers, he can make $3 \times 4 = 12$ outfits, one for each pair (shirt, trousers). In general, $|A \times B| = |A| \times |B|$. That is where the multiplication sign in $A \times B$ comes from.

Division with remainder sorts a set. Dividing $347$ eggs by $30$ splits the set of eggs into $11$ trays of $30$ and one leftover group of $17$. These groups do not overlap and together they contain every egg. A splitting like this is called a partition.

Think of "multiply by $3$" as a machine that changes any number into three times that number. Feed its output into a "multiply by $4$" machine, and the result is the same as one "multiply by $12$" machine. Chaining machines one after another is called composition (see one thing after another). The associative law says it does not matter how we bracket a chain of three machines. The machine "multiply by $1$" changes nothing. These two rules — brackets don't matter, and there is a do-nothing machine — are the rules that define a category, an idea you can explore much later.

• Egypt. The Rhind Mathematical Papyrus, copied by the scribe Ahmes around 1550 BCE from an older text, multiplies by doubling. To find $13 \times 12$: $12, 24, 48, 96$ are $1, 2, 4, 8$ times $12$, and $13 = 1 + 4 + 8$, so $13 \times 12 = 12 + 48 + 96 = 156$. This is the distributive law at work.
• Mesopotamia. Babylonian scribes, around 1800 BCE, worked in base $60$. They kept tables of products and tables of reciprocals. To divide by a number, they multiplied by its reciprocal.
• China. The Tsinghua bamboo slips, dated to about 305 BCE, contain a decimal multiplication table. It is the oldest one known anywhere in the world.
• Greece. Euclid's Elements (around 300 BCE) finds the greatest common measure of two numbers by subtracting the smaller from the larger again and again. Division with remainder is hidden inside this method.
• India and the Islamic world. Indian mathematicians developed decimal place value with a symbol for zero. Around 825 CE, Muḥammad ibn Mūsā al-Khwārizmī of Baghdad wrote a book on calculating with these "Hindu numerals". Its Latin translation spread the methods to Europe, and the word algorithm comes from his name.
• Today. In her book Knowing and Teaching Elementary Mathematics (1999), Liping Ma compared primary-school teachers in China and the United States. Many of the Chinese teachers, though they had spent fewer years in school, explained the methods through place value and the laws. She called this a "profound understanding of fundamental mathematics".

• Liping Ma, Knowing and Teaching Elementary Mathematics (1999). For teachers and parents; chapters 1–2 are about regrouping and multi-digit multiplication.
• Hung-Hsi Wu, Understanding Numbers in Elementary School Mathematics (2011). A careful account of why the standard algorithms work.
• Hans Magnus Enzensberger, The Number Devil (1997). A playful story about numbers for young readers.
• George Gheverghese Joseph, The Crest of the Peacock: Non-European Roots of Mathematics (1991). The history of calculation around the world.