Prodigious numbers

DefinitionProduct of the nonzero digits#✓fully proved

For natural numbers \(b\) and \(n\), this is the product of the nonzero digits of \(n\) in base \(b\); it equals \(1\) when \(n = 0\). In the degenerate bases, the digits of \(n > 0\) are the single digit \(n\) when \(b = 0\), and \(n\) copies of \(1\) when \(b = 1\).

public def nonzeroDigitProd (b n : ℕ) : ℕ :=
  ((Nat.digits b n).filter (· != 0)).prod

Used by 2

Used byChinese remainder solutions with nonzero-digit product one · Prodigious numbers

DefinitionProdigious numbers#✓fully proved

For natural numbers \(b\) and \(n\), the number \(n\) is \(b\)-prodigious when \(b \ge 2\), \(n > 0\), and \(n\) is divisible by the product of the nonzero digits of \(n\) in base \(b\).

public def IsProdigious (b n : ℕ) : Prop :=
  2 ≤ b ∧ 0 < n ∧ nonzeroDigitProd b n ∣ n

Uses 1

Statement usesProduct of the nonzero digits

TheoremChinese remainder solutions with nonzero-digit product one#✓fully proved

Let \(b \ge 3\) and \(w \ge 1\) be integers, and for \(v = 1, \dots, w\) let \(m_v\) be a positive integer and \(r_v\) an integer. Suppose the system of congruences \(x \equiv r_v \pmod{m_v}\), \(v = 1, \dots, w\), has an integer solution, and \(r_v = 0\) whenever \(\gcd(m_v, b) \ne 1\). Then the system has a positive integer solution \(c\) with \(p_b(c) = 1\), where \(p_b(c)\) is the product of the nonzero base-\(b\) digits of \(c\).

theorem exists_positive_crt_solution_nonzero_digit_product_one
    (w b : ℕ)
    (r : Fin w → ℤ)
    (m : Fin w → ℕ)
    (hw : 0 < w)
    (hb : 3 ≤ b)
    (hmpos : ∀ v, 0 < m v)
    (hconsistent : ∃ x : ℤ, ∀ v, Int.ModEq (m v : ℤ) x (r v))
    (hzero : ∀ v, Nat.gcd (m v) b ≠ 1 → r v = 0) :
    ∃ c : ℕ,
      0 < c ∧
        (∀ v, Int.ModEq (m v : ℤ) (c : ℤ) (r v)) ∧
          nonzeroDigitProd b c = 1

Sources

• Michael Gohn, Joshua Harrington, Sophia Lebiere, Hani Samamah, Kyla Shappell, and Tony W. H. Wong, "Arithmetic Progressions of b-Prodigious Numbers," Journal of Integer Sequences 25 (2022), Article 22.8.7, Lemma lem:crt, lines 178-180, https://cs.uwaterloo.ca/journals/JIS/VOL25/Wong/wong42.tex.

Uses 1

Statement usesProduct of the nonzero digits

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.