Divisibility by any prime

There is a delightful determinant test for divisibility by a prime, due to Watson Watson, 2003 and popularized by John D. Cook in Divisibility by any prime. To test whether an integer $n$ is divisible by a prime $p$ , split off the last digit, writing $n=10a+b$ , and evaluate a small $2\times 2$ determinant

\begin{vmatrix} a & b \\ k & 1 \end{vmatrix} = a - kb,

(1)

where $k$ is a fixed number depending only on $p$ . Then $n$ is divisible by $p$ if and only if this determinant is. Because the determinant is a smaller number, one simply iterates until divisibility is obvious.

This note explains why the test works, pins down the recipe for $k$ , and formalizes everything in Lean 4 + Mathlib.

The test in action¶

Take $p=31$ and $n=2759$ . Here 31 ends in 1, and the recipe below gives $k=3$ . Peel off the last digit and evaluate the determinant, then repeat:

\begin{vmatrix} 275 & 9 \\ 3 & 1 \end{vmatrix} = 275 - 3\cdot 9 = 248, \qquad \begin{vmatrix} 24 & 8 \\ 3 & 1 \end{vmatrix} = 24 - 3\cdot 8 = 0.

(2)

The chain ends in 0, which is divisible by 31, so 2759 is divisible by 31.

For a negative answer, take $p=61$ and $n=75273$ . Again 61 ends in 1, giving $k=6$ :

\begin{vmatrix} 7527 & 3 \\ 6 & 1 \end{vmatrix} = 7509,\quad \begin{vmatrix} 750 & 9 \\ 6 & 1 \end{vmatrix} = 696,\quad \begin{vmatrix} 69 & 6 \\ 6 & 1 \end{vmatrix} = 33.

(3)

Since 33 is not divisible by 61, neither is 75273.

The determinant is literally $a-kb$ ; the Lean statement below checks this against Mathlib’s own $2\times 2$ determinant.

DivisibilityByPrimeFlow.lean

/-- The determinant appearing in the test is `a - k * b`:
`det ![![a, b], ![k, 1]] = a * 1 - b * k = a - k * b`. -/
theorem det_eq (a b k : ℤ) : Matrix.det !![a, b; k, 1] = a - k * b := by
  rw [Matrix.det_fin_two_of]; ring

Why it works¶

Let $p$ be an integer and split $n=10a+b$ . Suppose $k$ is chosen so that

10k+1=mp \qquad\text{for some integer } m,

(4)

i.e. $10k\equiv-1\pmod p$ . The whole test rests on one algebraic identity:

10\,(a-kb)=(10a+b)-(10k+1)\,b.

(5)

Indeed, expanding the right-hand side gives $10a+b-10kb-b=10a-10kb=10(a-kb)$ .

The equivalence. Working modulo $p$ , the term $(10k+1)b$ vanishes by (4), so (5) says

10\,(a-kb)\equiv 10a+b=n \pmod p.

(6)

Now 10 is invertible modulo $p$ — the certificate (4) rearranges to $(-k)\cdot 10+m\cdot p=1$ , a Bézout identity proving $\gcd(10,p)=1$ — so multiplying by 10 neither creates nor destroys divisibility by $p$ . Therefore

p \mid (10a+b) \iff p \mid (a-kb).

(7)

Read left to right: if $p\mid 10a+b$ then $p$ divides the right-hand side of (5), hence $p\mid 10(a-kb)$ , and coprimality gives $p\mid a-kb$ . Read right to left: if $p\mid a-kb$ then $p\mid 10(a-kb)$ , and adding the multiple $(10k+1)b$ of $p$ gives $p\mid 10a+b$ ; this direction needs no coprimality.

DivisibilityByPrimeFlow.lean

/-- **The heart of the method.**  If `10 * k + 1 = m * p` for some integer `m`, then for all `a b`,
`p` divides `10 * a + b` **iff** `p` divides the determinant `a - k * b`.

The forward direction uses `10 * (a - k * b) = (10 * a + b) - (10 * k + 1) * b` together with
coprimality of `10` and `p` (itself supplied by the certificate); the converse uses the same
identity read backwards and needs no coprimality. -/
theorem dvd_iff {p k m : ℤ} (hmp : 10 * k + 1 = m * p) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ (a - k * b) := by
  have hpk : p ∣ (10 * k + 1) := ⟨m, by linear_combination hmp⟩
  have hcop : IsCoprime p 10 := (isCoprime_ten hmp).symm
  constructor
  · intro hdvd
    have key : 10 * (a - k * b) = (10 * a + b) - (10 * k + 1) * b := by ring
    have h1 : p ∣ 10 * (a - k * b) := by
      rw [key]; exact dvd_sub hdvd (hpk.mul_right b)
    exact hcop.dvd_of_dvd_mul_left h1
  · intro hdvd
    have key : 10 * a + b = 10 * (a - k * b) + (10 * k + 1) * b := by ring
    rw [key]
    exact dvd_add (hdvd.mul_left 10) (hpk.mul_right b)

DivisibilityByPrimeFlow.lean

/-- The core equivalence phrased with the literal determinant: `p ∣ 10 * a + b` iff `p` divides
`det ![![a, b], ![k, 1]]`. -/
theorem dvd_iff_dvd_det {p k m : ℤ} (hmp : 10 * k + 1 = m * p) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ Matrix.det !![a, b; k, 1] := by
  rw [det_eq]; exact dvd_iff hmp a b

The Lean dvd_iff takes the single hypothesis 10 * k + 1 = m * p and returns (7); key is exactly the identity (5).

Note that (7) used nothing about $p$ except that (4) has a solution — equivalently, that $\gcd(10,p)=1$ . Primality is not needed for the equivalence itself; it enters only when we guarantee a $k$ exists and is easy to compute.

DivisibilityByPrimeFlow.lean

/-- The certificate `10 * k + 1 = m * p` is a Bézout identity `(-k) * 10 + m * p = 1`, so it forces
`10` and `p` to be coprime.  Equivalently, this is why the method needs `p` to end in `1, 3, 7, 9`:
those are exactly the last digits for which `p` is coprime to `10`. -/
theorem isCoprime_ten {p k m : ℤ} (hmp : 10 * k + 1 = m * p) : IsCoprime (10 : ℤ) p :=
  ⟨-k, m, by linear_combination -hmp⟩

The certificate $10k+1=mp$ is the Bézout witness $(-k)\cdot 10+m\cdot p=1$ , so Lean derives IsCoprime 10 p from it directly, with no separate assumption.

Finding $k$ ¶

We need $k$ with $10k\equiv-1\pmod p$ . Since $\gcd(10,p)=1$ exactly when the last digit of $p$ is $1,3,7,9$ , these four cases cover all odd primes except 5. In each case there is a small multiplier $m$ with $mp\equiv 1\pmod{10}$ — namely the inverse of the last digit modulo 10, using $1\cdot1\equiv3\cdot7\equiv9\cdot9\equiv1$ — and then $k=\lfloor mp/10\rfloor$ , so that $10k+1=mp$ is a multiple of $p$ :

last digit of $p$	multiplier $m$	$k$	certificate $10k+1$
1	1	$\lfloor p/10\rfloor$	$1\cdot p$
3	7	$\lfloor 7p/10\rfloor$	$7\cdot p$
7	3	$\lfloor 3p/10\rfloor$	$3\cdot p$
9	9	$\lfloor 9p/10\rfloor$	$9\cdot p$

For example, if $p$ ends in 3 then $7p$ ends in 1 (because $7\cdot 3=21$ ), so $7p=10\lfloor 7p/10\rfloor+1$ ; taking $k=\lfloor 7p/10\rfloor$ gives $10k+1=7p$ , a multiple of $p$ . The other rows are identical with 7 replaced by the relevant multiplier. This is where the earlier example $k=3$ for $p=31$ comes from ( $\lfloor 31/10\rfloor=3$ ), and $k=6$ for $p=61$ ( $\lfloor 61/10\rfloor=6$ ).

DivisibilityByPrimeFlow.lean

/-- If `p` ends in `1`, then `k = ⌊p / 10⌋` satisfies the certificate `10 * k + 1 = 1 * p`. -/
theorem k_digit_one {p : ℤ} (hp : p % 10 = 1) : 10 * (p / 10) + 1 = 1 * p := by omega

/-- If `p` ends in `3`, then `k = ⌊7 * p / 10⌋` satisfies the certificate `10 * k + 1 = 7 * p`. -/
theorem k_digit_three {p : ℤ} (hp : p % 10 = 3) : 10 * (7 * p / 10) + 1 = 7 * p := by omega

/-- If `p` ends in `7`, then `k = ⌊3 * p / 10⌋` satisfies the certificate `10 * k + 1 = 3 * p`. -/
theorem k_digit_seven {p : ℤ} (hp : p % 10 = 7) : 10 * (3 * p / 10) + 1 = 3 * p := by omega

/-- If `p` ends in `9`, then `k = ⌊9 * p / 10⌋` satisfies the certificate `10 * k + 1 = 9 * p`. -/
theorem k_digit_nine {p : ℤ} (hp : p % 10 = 9) : 10 * (9 * p / 10) + 1 = 9 * p := by omega

Each states the certificate (4) for the prescribed $k$ ; omega discharges the floor-division arithmetic.

Feeding each certificate into the core equivalence gives four ready-to-use tests.

DivisibilityByPrimeFlow.lean

/-- Divisibility test for a `p` ending in `1`. -/
theorem test_digit_one {p : ℤ} (hp : p % 10 = 1) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ (a - (p / 10) * b) :=
  dvd_iff (k_digit_one hp) a b

/-- Divisibility test for a `p` ending in `3`. -/
theorem test_digit_three {p : ℤ} (hp : p % 10 = 3) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ (a - (7 * p / 10) * b) :=
  dvd_iff (k_digit_three hp) a b

/-- Divisibility test for a `p` ending in `7`. -/
theorem test_digit_seven {p : ℤ} (hp : p % 10 = 7) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ (a - (3 * p / 10) * b) :=
  dvd_iff (k_digit_seven hp) a b

/-- Divisibility test for a `p` ending in `9`. -/
theorem test_digit_nine {p : ℤ} (hp : p % 10 = 9) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ (a - (9 * p / 10) * b) :=
  dvd_iff (k_digit_nine hp) a b

For instance, test_digit_seven says that for $p$ ending in 7, $p\mid 10a+b \iff p\mid a-\lfloor 3p/10\rfloor\,b$ .

The main theorem¶

Combining the equivalence (7) with the recipe for $k$ folds all four cases into a single statement. Write $k(p)$ for the number produced by the table in Finding $k$ — a function of $p$ alone.

In Lean the number $k(p)$ is kFor p, defined by the four-way case split on the last digit, and the theorem divisibility_test is a two-line consequence of the core equivalence dvd_iff_dvd_det together with the certificate $10\,k(p)+1=m\,p$ that the case split supplies.

DivisibilityByPrimeFlow.lean

/-- The number `k` used in the test, as a function of `p` alone.  It depends only on the last digit
of `p`, following the table: the multiplier `m ∈ {1, 7, 3, 9}` is the inverse of that digit modulo
`10`, and `k = ⌊m * p / 10⌋`. -/
def kFor (p : ℤ) : ℤ :=
  if p % 10 = 1 then p / 10          -- m = 1
  else if p % 10 = 3 then 7 * p / 10 -- m = 7
  else if p % 10 = 7 then 3 * p / 10 -- m = 3
  else 9 * p / 10                    -- m = 9

/-- **Main theorem (divisibility test).**  Let `p` be an integer whose last digit is `1, 3, 7`, or
`9` — for a prime, exactly every prime other than `2` and `5`.  Writing `n = 10 * a + b`, the number
`p` divides `n` **if and only if** `p` divides the determinant

  `| a       b |`
  `| kFor p  1 |  =  a - (kFor p) * b`. -/
theorem divisibility_test {p : ℤ}
    (hp : p % 10 = 1 ∨ p % 10 = 3 ∨ p % 10 = 7 ∨ p % 10 = 9) (a b : ℤ) :
    p ∣ (10 * a + b) ↔ p ∣ Matrix.det !![a, b; kFor p, 1] := by
  have hcert : ∃ m : ℤ, 10 * kFor p + 1 = m * p := by
    unfold kFor
    split_ifs with h1 h3 h7
    · exact ⟨1, by omega⟩
    · exact ⟨7, by omega⟩
    · exact ⟨3, by omega⟩
    · exact ⟨9, by omega⟩
  obtain ⟨m, hm⟩ := hcert
  exact dvd_iff_dvd_det hm a b

The statement reads exactly as the informal one: p ∣ (10 * a + b) iff p divides Matrix.det !![a, b; kFor p, 1], Mathlib’s $2\times2$ determinant $a-k(p)\,b$ .

The worked examples, formalized¶

The same reductions used above can be run inside Lean. Applying the core equivalence with the explicit certificate at each step turns the divisibility question into a chain of equivalences ending in an obvious case.

For $p=37$ (which ends in 7, so $k=\lfloor 3\cdot 37/10\rfloor=11$ ) and $n=3293$ , this is Cook’s headline example:

\begin{vmatrix} 329 & 3 \\ 11 & 1 \end{vmatrix} = 296,\qquad \begin{vmatrix} 29 & 6 \\ 11 & 1 \end{vmatrix} = 29 - 66 = -37,

(9)

and -37 is divisible by 37. (The blog writes the last determinant as 37; its sign is irrelevant because we only ask about divisibility.)

DivisibilityByPrimeFlow.lean

/-- `31` ends in `1`, so `k = 3` (certificate `10 * 3 + 1 = 1 * 31`).  The method reduces `2759`
to `0`: `|275 9; 3 1| = 248`, then `|24 8; 3 1| = 0`. -/
theorem reduce_2759 : (31 : ℤ) ∣ 2759 ↔ (31 : ℤ) ∣ 0 := by
  rw [show (2759 : ℤ) = 10 * 275 + 9 by norm_num,
      dvd_iff (show (10 : ℤ) * 3 + 1 = 1 * 31 by norm_num) 275 9,
      show (275 : ℤ) - 3 * 9 = 10 * 24 + 8 by norm_num,
      dvd_iff (show (10 : ℤ) * 3 + 1 = 1 * 31 by norm_num) 24 8,
      show (24 : ℤ) - 3 * 8 = 0 by norm_num]

/-- Hence `31 ∣ 2759`. -/
theorem dvd_2759 : (31 : ℤ) ∣ 2759 := reduce_2759.mpr (dvd_zero 31)

/-- `37` ends in `7`, so `k = ⌊3 · 37 / 10⌋ = 11` (certificate `10 * 11 + 1 = 3 * 37`).  The method
reduces `3293` to `-37`: `|329 3; 11 1| = 296`, then `|29 6; 11 1| = -37`. -/
theorem reduce_3293 : (37 : ℤ) ∣ 3293 ↔ (37 : ℤ) ∣ (-37) := by
  rw [show (3293 : ℤ) = 10 * 329 + 3 by norm_num,
      dvd_iff (show (10 : ℤ) * 11 + 1 = 3 * 37 by norm_num) 329 3,
      show (329 : ℤ) - 11 * 3 = 10 * 29 + 6 by norm_num,
      dvd_iff (show (10 : ℤ) * 11 + 1 = 3 * 37 by norm_num) 29 6,
      show (29 : ℤ) - 11 * 6 = -37 by norm_num]

/-- Hence `37 ∣ 3293` (the sign of the last determinant is irrelevant to divisibility). -/
theorem dvd_3293 : (37 : ℤ) ∣ 3293 := reduce_3293.mpr ⟨-1, by norm_num⟩

/-- `61` ends in `1`, so `k = 6` (certificate `10 * 6 + 1 = 1 * 61`).  The method reduces `75273`
to `33`: `7509`, then `696`, then `33`. -/
theorem reduce_75273 : (61 : ℤ) ∣ 75273 ↔ (61 : ℤ) ∣ 33 := by
  rw [show (75273 : ℤ) = 10 * 7527 + 3 by norm_num,
      dvd_iff (show (10 : ℤ) * 6 + 1 = 1 * 61 by norm_num) 7527 3,
      show (7527 : ℤ) - 6 * 3 = 10 * 750 + 9 by norm_num,
      dvd_iff (show (10 : ℤ) * 6 + 1 = 1 * 61 by norm_num) 750 9,
      show (750 : ℤ) - 6 * 9 = 10 * 69 + 6 by norm_num,
      dvd_iff (show (10 : ℤ) * 6 + 1 = 1 * 61 by norm_num) 69 6,
      show (69 : ℤ) - 6 * 6 = 33 by norm_num]

/-- Since `61 ∤ 33`, the number `75273` is **not** divisible by `61`. -/
theorem not_dvd_75273 : ¬ (61 : ℤ) ∣ 75273 := by rw [reduce_75273]; omega

reduce_2759 reduces $31\mid 2759$ to $31\mid 0$ , reduce_3293 reduces $37\mid 3293$ to $37\mid -37$ , and reduce_75273 reduces $61\mid 75273$ to $61\mid 33$ — from which dvd_2759, dvd_3293, and not_dvd_75273 read off the answers.

Summary¶

To test $n=10a+b$ for divisibility by a prime $p$ ending in $1,3,7,9$ : pick $k$ from the table in Finding $k$ , replace $n$ by the determinant $a-kb$ , and repeat. The number $n$ is divisible by $p$ if and only if the final determinant is. The mechanism is the single identity (5) together with the fact that 10 is invertible modulo any $p$ coprime to 10, which the last-digit condition guarantees.

References¶

Watson, R. A. (2003). Tests for Divisibility. The Mathematical Gazette, 87(510), 493–494.

Divisibility by any prime

The test in action¶

Why it works¶

Finding kkk¶

The main theorem¶

The worked examples, formalized¶

Summary¶

Finding $k$ ¶