Sylvester's coin theorem

TheoremSylvester's coin theorem for two distinct odd primes#✓fully proved

Let \(p\) and \(q\) be distinct odd primes. Then the number of natural numbers \(n\) that cannot be written as \(n = px + qy\) with natural numbers \(x, y\) is \((p-1)(q-1)/2\).

Distinct odd primes are coprime, so this is a special case of Sylvester's count for coprime \(p\) and \(q\).

theorem sylvester_coin_distinct_odd_primes
    (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q)
    (hodd : Odd p ∧ Odd q) (hne : p ≠ q) :
    Nat.card { n : ℕ // ¬ ∃ x y : ℕ, n = p * x + q * y }
      = (p - 1) * (q - 1) / 2

Sources

• Damanvir Singh Binner, "Generalization of a Result of Sylvester Related to the Frobenius Coin Problem", Journal of Integer Sequences 24 (2021), Article 21.8.4, Theorem Sylvester' (the Special Case of Sylvester's theorem), source lines 123–127, https://cs.uwaterloo.ca/journals/JIS/VOL24/Binner/binner13.tex. The paper attributes the general coprime statement to Sylvester (1882).

TheoremSylvester's coin theorem#✓fully proved

Let \(a\) and \(b\) be coprime natural numbers. Then the number of natural numbers \(n\) that cannot be written as \(n = ax + by\) with natural numbers \(x, y\) is \((a - 1)(b - 1)/2\).

Subtraction here is truncated at \(0\): if \(a = 0\) or \(b = 0\), coprimality forces the other number to be \(1\), every natural number is representable, and both sides are \(0\).

theorem sylvester_coin_theorem
    (a b : ℕ) (hab : Nat.Coprime a b) :
    {n : ℕ | ¬ ∃ x y : ℕ, n = a * x + b * y}.ncard =
      (a - 1) * (b - 1) / 2

Sources

• J. J. Sylvester on the Frobenius coin problem (1882); the count of gaps is (a - 1) * (b - 1) / 2 for coprime a b.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.