Number theory

Why the digit test for 3 works

Prove the single step behind a familiar school arithmetic trick.

-- Top 100 #85: Why the digit test for 3 works
-- History: First discovery date unknown.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The decimal base 10 leaves remainder 1 modulo 3.
-- Scope: Proves that replacing n with its last digit plus the remaining prefix preserves its residue modulo 3. Iteration gives the digit-sum rule.
-- Source: https://lurch.plus/100/

theorem digit_step (n : Nat) :
    n % 3 = (n / 10 + n % 10) % 3 := by
  omega

-- Apply the step to 123: replace it with 12+3.
example : 123 % 3 = (12+3) % 3 := by decide
-- Repeat until the result is small.
example : (12+3) % 3 = (1+2+3) % 3 := by decide

Explanation

`%`

Remainder after division. n % 3 is 0, 1, or 2.

`/`

Division on Nat is integer division; n / 10 drops the final decimal digit.

`omega`

A core tactic for linear integer/natural arithmetic, including division and remainders by constants.

Background and proof scope

First discovery date unknown

The decimal base 10 leaves remainder 1 modulo 3.

Proves that replacing n with its last digit plus the remaining prefix preserves its residue modulo 3. Iteration gives the digit-sum rule.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Replace 3 with 9. Does the same theorem hold? What happens for 7?