Reverse multiples

TheoremSloane's endpoint formula for reverse multiples#✓fully proved

Let \(g\) and \(k\) be integers with \(2 \le k < g\), and let \(N = (a_n a_{n-1} \cdots a_0)_g\) have base-\(g\) digits \(a_0, \dots, a_n \in \{0, \dots, g - 1\}\), with units digit \(a_0\) and leading digit \(a_n \ne 0\). Suppose \(N\) is a \((g, k)\) reverse multiple, that is, \(k N = (a_0 a_1 \cdots a_n)_g\), and that \(a_0 + a_n = g\). Then \((k + 1) a_n = g\); in particular \(k + 1\) divides \(g\) and \(a_n = g / (k + 1)\).

theorem sloane_reverse_multiple_endpoint
    (g k a₀ aLast : ℕ) (digits : List ℕ)
    (hk : 2 ≤ k) (hkg : k < g)
    (hdigits : ∀ d ∈ digits, d < g)
    (hunits : digits.head? = some a₀)
    (hleading : digits.getLast? = some aLast)
    (hleading_ne : aLast ≠ 0)
    (hreverse : k * Nat.ofDigits g digits = Nat.ofDigits g digits.reverse)
    (hendpoint_sum : a₀ + aLast = g) :
    (k + 1) * aLast = g ∧ aLast = g / (k + 1) ∧ k + 1 ∣ g
Sources

TheoremSutcliffe's theorem on two- and three-digit reverse multiples#✓fully proved

Let \(g\) and \(k\) be integers with \(2 \le k < g\), and let \(a\) and \(b\) be base-\(g\) digits, \(0 \le a, b < g\), with \(a \ne 0\), such that \((a\,b)_g\) is a \((g, k)\) reverse multiple, that is, \(k (a g + b) = b g + a\). Then \(a + b < g\), so \(a + b\) is a base-\(g\) digit, and \((a\,(a + b)\,b)_g\) is again a \((g, k)\) reverse multiple, that is, \(k (a g^2 + (a + b) g + b) = b g^2 + (a + b) g + a\).

This is the forward implication of Sutcliffe's theorem; the converse is not included.

theorem sutcliffe_two_to_three_digit_reverse_multiple
    (g k a b : ℕ)
    (hk : 2 ≤ k) (hkg : k < g)
    (ha : a ≠ 0) (hag : a < g) (hbg : b < g)
    (hreverse : k * (a * g + b) = b * g + a) :
    a + b < g ∧
      k * (a * g ^ 2 + (a + b) * g + b) =
        b * g ^ 2 + (a + b) * g + a
Sources

DefinitionRetained node#✓fully proved

Let \(V\) be a set, let \(P\) be a predicate on \(V\) (the pivot nodes) and let \(\prec\) be a binary relation on \(V\). A node \(v \in V\) is retained with respect to \(P\) and \(\prec\) if \(P(v)\) holds or there is a node \(w \in V\) with \(P(w)\) and \(v \prec w\).

def isYoungRetained {V : Type _} (pivot : V → Prop)
    (precedes : V → V → Prop) (v : V) : Prop :=
  pivot v ∨ ∃ w, pivot w ∧ precedes v w
Used by 5
Used byCharacterization of retained nodes · Young graph of a labeled directed graph · Label of an edge in the Young graph · Source of an edge in the Young graph · Target of an edge in the Young graph

TheoremCharacterization of retained nodes#✓fully proved

Let \(V\) be a set, let \(P\) be a predicate on \(V\) and let \(\prec\) be a binary relation on \(V\). A node \(v \in V\) is retained with respect to \(P\) and \(\prec\) if and only if \(P(v)\) holds or there is a node \(w \in V\) with \(P(w)\) and \(v \prec w\).

@[simp]
theorem isYoungRetained_iff {V : Type _} (pivot : V → Prop)
    (precedes : V → V → Prop) (v : V) :
    isYoungRetained pivot precedes v ↔ pivot v ∨ ∃ w, pivot w ∧ precedes v w
Uses 1
Statement usesRetained node

DefinitionYoung graph of a labeled directed graph#✓fully proved

Let \(G\) be a labeled directed graph with vertex set \(V\), edge set \(E\) and label set \(L\), let \(P\) be a predicate on \(V\) and let \(\prec\) be a binary relation on \(V\). The Young graph of \(G\) with respect to \(P\) and \(\prec\) is the labeled directed graph with label set \(L\) whose vertices are the vertices of \(G\) that are retained with respect to \(P\) and \(\prec\), whose edges are the edges of \(G\) whose source and target are both retained, and in which each edge has the same source, target and label as in \(G\).

def youngGraph {V E L : Type _} (G : LabeledDigraph V E L)
    (pivot : V → Prop) (precedes : V → V → Prop) :
    LabeledDigraph { v : V // isYoungRetained pivot precedes v }
      { e : E // isYoungRetained pivot precedes (G.src e) ∧
        isYoungRetained pivot precedes (G.tgt e) } L :=
  G.restrict (isYoungRetained pivot precedes)
Uses 3 · Used by 3
Statement usesLabeled directed graph · Restriction of a labeled directed graph · Retained node
Used byLabel of an edge in the Young graph · Source of an edge in the Young graph · Target of an edge in the Young graph

TheoremSource of an edge in the Young graph#✓fully proved

Let \(G\) be a labeled directed graph, let \(P\) be a predicate on its vertices, let \(\prec\) be a binary relation on its vertices, and let \(e\) be an edge of \(G\) whose source and target are both retained with respect to \(P\) and \(\prec\), viewed as an edge of the Young graph of \(G\) with respect to \(P\) and \(\prec\). The source of \(e\) in the Young graph, viewed as a vertex of \(G\), is the source of \(e\) in \(G\).

@[simp]
theorem youngGraph_src {V E L : Type _} (G : LabeledDigraph V E L)
    (pivot : V → Prop) (precedes : V → V → Prop)
    (e : {e : E // isYoungRetained pivot precedes (G.src e) ∧
      isYoungRetained pivot precedes (G.tgt e)}) :
    ((youngGraph G pivot precedes).src e).val = G.src e.val
Uses 3
Statement usesLabeled directed graph · Retained node · Young graph of a labeled directed graph

TheoremTarget of an edge in the Young graph#✓fully proved

Let \(G\) be a labeled directed graph, let \(P\) be a predicate on its vertices, let \(\prec\) be a binary relation on its vertices, and let \(e\) be an edge of \(G\) whose source and target are both retained with respect to \(P\) and \(\prec\), viewed as an edge of the Young graph of \(G\) with respect to \(P\) and \(\prec\). The target of \(e\) in the Young graph, viewed as a vertex of \(G\), is the target of \(e\) in \(G\).

@[simp]
theorem youngGraph_tgt {V E L : Type _} (G : LabeledDigraph V E L)
    (pivot : V → Prop) (precedes : V → V → Prop)
    (e : {e : E // isYoungRetained pivot precedes (G.src e) ∧
      isYoungRetained pivot precedes (G.tgt e)}) :
    ((youngGraph G pivot precedes).tgt e).val = G.tgt e.val
Uses 3
Statement usesLabeled directed graph · Retained node · Young graph of a labeled directed graph

TheoremLabel of an edge in the Young graph#✓fully proved

Let \(G\) be a labeled directed graph, let \(P\) be a predicate on its vertices, let \(\prec\) be a binary relation on its vertices, and let \(e\) be an edge of \(G\) whose source and target are both retained with respect to \(P\) and \(\prec\), viewed as an edge of the Young graph of \(G\) with respect to \(P\) and \(\prec\). The label of \(e\) in the Young graph is its label in \(G\).

@[simp]
theorem youngGraph_label {V E L : Type _} (G : LabeledDigraph V E L)
    (pivot : V → Prop) (precedes : V → V → Prop)
    (e : {e : E // isYoungRetained pivot precedes (G.src e) ∧
      isYoungRetained pivot precedes (G.tgt e)}) :
    (youngGraph G pivot precedes).label e = G.label e.val
Uses 3
Statement usesLabeled directed graph · Retained node · Young graph of a labeled directed graph

TheoremCarry equations for reverse multiples, general form#✓fully proved

Let \(g, k, n\) be natural numbers with \(2 \le k < g\), and let \(a_0, \dots, a_{n-1}\) be natural numbers with \(a_i < g\) for every \(i\). Then \(k \sum_{i\lt n} a_i g^i = \sum_{i\lt n} a_{n-1-i} g^i\) if and only if there is a unique sequence of natural numbers \(r_0, \dots, r_n\) with \(r_0 = 0\), \(r_n = 0\) and, for every \(i < n\), \(r_{i+1} < k\) and \(k a_i + r_i = a_{n-1-i} + r_{i+1} g\).

No hypothesis is placed on \(n\) or on the end digits \(a_0\) and \(a_{n-1}\); in particular \(n\) may be \(0\).

theorem young_reverse_multiple_carry_path_iff_general
    (g k n : ℕ) (hgk : 2 ≤ k) (hkg : k < g)
    (a : Fin n → ℕ) (hdigit : ∀ i, a i < g) :
    k * (∑ i, a i * g ^ i.val) = ∑ i, a (Fin.rev i) * g ^ i.val ↔
      ∃! r : Fin (n + 1) → ℕ,
        r ⟨0, Nat.succ_pos n⟩ = 0 ∧ r (Fin.last n) = 0 ∧
          ∀ i : Fin n, r i.succ < k ∧
            k * a i + r i.castSucc = a (Fin.rev i) + r i.succ * g
Used by 1
Used byCarry equations for reverse multiples

TheoremCarry equations for reverse multiples#✓fully proved

Let \(g, k, n\) be natural numbers with \(2 \le k < g\) and \(n \ge 1\), and let \(a_0, \dots, a_{n-1}\) be natural numbers with \(a_i < g\) for every \(i\), \(a_{n-1} \ne 0\) and \(a_0 \ne 0\). Then \(k \sum_{i\lt n} a_i g^i = \sum_{i\lt n} a_{n-1-i} g^i\), that is, \(k\) times the number with base-\(g\) digits \(a_{n-1}, \dots, a_0\) (most significant first) equals the number with these digits reversed, if and only if there is a unique sequence of natural numbers \(r_0, \dots, r_n\) with \(r_0 = 0\), \(r_n = 0\) and, for every \(i < n\), \(r_{i+1} < k\) and \(k a_i + r_i = a_{n-1-i} + r_{i+1} g\).

The carry \(r_{i+1}\) here is the source's \(r_i\).

theorem young_reverse_multiple_carry_path_iff
    (g k n : ℕ) (hgk : 2 ≤ k) (hkg : k < g) (hn : 0 < n)
    (a : Fin n → ℕ) (hdigit : ∀ i, a i < g)
    (hfirst : a (Fin.rev ⟨0, hn⟩) ≠ 0) (hlast : a ⟨0, hn⟩ ≠ 0) :
    k * (∑ i, a i * g ^ i.val) = ∑ i, a (Fin.rev i) * g ^ i.val ↔
      ∃! r : Fin (n + 1) → ℕ,
        r ⟨0, Nat.succ_pos n⟩ = 0 ∧ r (Fin.last n) = 0 ∧
          ∀ i : Fin n, r i.succ < k ∧
            k * a i + r i.castSucc = a (Fin.rev i) + r i.succ * g
Sources
  • L. H. Kendrick, Young Graphs: 1089 et al., Journal of Integer Sequences 18 (2015), Article 15.9.7, subsection subsec:eqtns, lines 128–154 (the column equations for kN = Reverse_g(N), Young's bound r_i ≤ k - 1, and equation eq:rmdig), https://cs.uwaterloo.ca/journals/JIS/VOL18/Kendrick/ken1.tex. It follows from young_reverse_multiple_carry_path_iff_general; the hypotheses hfirst and hlast (and hn, which only serves to state them) are unused and keep the source's shape.
Uses 1
Proof usesCarry equations for reverse multiples, general form

TheoremYoung's theorem on reverse multiples#✓fully proved

Let \(g\) and \(k\) be natural numbers with \(2 \le k < g\). A \((g, k)\) reverse multiple is a list of base-\(g\) digits \(d_1, d_2, \dots, d_n\), most significant first, with \(n \ge 2\), \(d_1 \ne 0\), \(d_n \ne 0\) and \(d_i < g\) for every \(i\), such that \(k\) times the number \(\sum_{i=1}^{n} d_i g^{n-i}\) equals the number \(\sum_{i=1}^{n} d_{n+1-i} g^{n-i}\) whose digits are those of the first in reverse order. Consider the graph whose nodes are pairs \((r, s)\) of natural numbers, with an edge labeled \((a, b)\) from \((r, s)\) to \((r', s')\) whenever \(k b + s = a + s' g\) and \(k a + r' = b + r g\). A path is a sequence of nodes \(v_0, \dots, v_m\) together with a sequence of labels \(\ell_1, \dots, \ell_m\) such that \(m \ge 1\), \(v_0 = (0, 0)\), both coordinates of every node are less than \(k\), both coordinates of every label are less than \(g\), both coordinates of \(\ell_1\) are nonzero, and for each \(j\) the label \(\ell_j\) labels an edge from \(v_{j-1}\) to \(v_j\). A node \((r, s)\) is an even pivot if \(r = s\), and an odd pivot if for some \(c < g\) there is an edge labeled \((c, c)\) from \((r, s)\) to \((s, r)\).

Then there is a bijection from the \((g, k)\) reverse multiples with an even number of digits to the paths whose last node is an even pivot, and a bijection from the \((g, k)\) reverse multiples with an odd number of digits to the paths whose last node is an odd pivot. Under both bijections, a reverse multiple \(d_1, \dots, d_n\) is sent to a path with labels \((d_1, d_n), (d_2, d_{n-1}), \dots, (d_h, d_{n+1-h})\), where \(h = \lfloor n/2 \rfloor\); in the odd case, if \((r, s)\) is the last node of that path, there is an edge labeled \((d_{h+1}, d_{h+1})\) from \((r, s)\) to \((s, r)\).

MetaMathlibExt.young_reverse_multiples_equiv_pivot_paths · 52 lines 
theorem young_reverse_multiples_equiv_pivot_paths
    (g k : ℕ) (hk : 2 ≤ k) (hkg : k < g) :
    let digitValue := fun digits : List ℕ =>
      digits.foldl (fun value digit => value * g + digit) 0
    let IsReverseMultiple := fun digits : List ℕ =>
      (∃ first middle last,
          digits = first :: middle ++ [last] ∧ first ≠ 0 ∧ last ≠ 0) ∧
        (∀ digit ∈ digits, digit < g) ∧
        k * digitValue digits = digitValue digits.reverse
    let Transition := fun (source : ℕ × ℕ) (label : ℕ × ℕ) (target : ℕ × ℕ) =>
      k * label.2 + source.2 = label.1 + target.2 * g ∧
        k * label.1 + target.1 = label.2 + source.1 * g
    let IsPath := fun path : List (ℕ × ℕ) × List (ℕ × ℕ) =>
      path.2.length = path.1.length + 1 ∧
        path.2.head? = some (0, 0) ∧
        (∀ node ∈ path.2, node.1 < k ∧ node.2 < k) ∧
        (∀ label ∈ path.1, label.1 < g ∧ label.2 < g) ∧
        (∃ first rest,
          path.1 = first :: rest ∧ first.1 ≠ 0 ∧ first.2 ≠ 0) ∧
        List.Forall₂
          (fun label endpoints => Transition endpoints.1 label endpoints.2)
          path.1 (path.2.zip path.2.tail)
    let EvenReverseMultiples :=
      {digits : List ℕ // IsReverseMultiple digits ∧ Even digits.length}
    let OddReverseMultiples :=
      {digits : List ℕ // IsReverseMultiple digits ∧ Odd digits.length}
    let PathsToEvenPivots :=
      {path : List (ℕ × ℕ) × List (ℕ × ℕ) //
        IsPath path ∧ ∃ r, path.2.getLast? = some (r, r)}
    let PathsToOddPivots :=
      {path : List (ℕ × ℕ) × List (ℕ × ℕ) //
        IsPath path ∧
          ∃ r s middle,
            path.2.getLast? = some (r, s) ∧ middle < g ∧
              Transition (r, s) (middle, middle) (s, r)}
    ∃ evenCorrespondence : EvenReverseMultiples ≃ PathsToEvenPivots,
      ∃ oddCorrespondence : OddReverseMultiples ≃ PathsToOddPivots,
        (∀ reverseMultiple,
          (evenCorrespondence reverseMultiple).1.1 =
            List.zip
              (reverseMultiple.1.take (reverseMultiple.1.length / 2))
              (reverseMultiple.1.reverse.take (reverseMultiple.1.length / 2))) ∧
        (∀ reverseMultiple,
          (oddCorrespondence reverseMultiple).1.1 =
              List.zip
                (reverseMultiple.1.take (reverseMultiple.1.length / 2))
                (reverseMultiple.1.reverse.take (reverseMultiple.1.length / 2)) ∧
            ∃ middle r s,
              (reverseMultiple.1.drop (reverseMultiple.1.length / 2)).head? =
                some middle ∧
              (oddCorrespondence reverseMultiple).1.2.getLast? = some (r, s) ∧
              Transition (r, s) (middle, middle) (s, r))
Sources

DefinitionReverse divisor#✓fully proved

A natural number \(n\) is a reverse divisor if \(n > 0\) and there is a natural number \(k \ge 2\) such that the decimal reversal of \(n\) equals \(kn\). Since \(n > 0\), such a \(k\) is unique; it is called the quotient of \(n\).

def IsReverseDivisor (n : ℕ) : Prop :=
  0 < n ∧ ∃ k : ℕ, 2 ≤ k ∧ Nat.reverseDigits 10 n = k * n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Section 1 (terminology).
Uses 1 · Used by 6
Statement usesDigit reversal
Used byReverse divisors with at most seven digits · Sufficient conditions for a multiple with divisible reversal · Reverse divisors have at least four digits · Characterization of reverse divisors · No reverse divisor has property \(P^*\) · Reverse divisors have quotient \(4\) or \(9\)

TheoremCharacterization of reverse divisors#✓fully proved

A natural number \(n\) is a reverse divisor if and only if \(n > 0\) and there is a natural number \(k \ge 2\) such that the decimal reversal of \(n\) equals \(kn\).

theorem isReverseDivisor_iff (n : ℕ) :
    IsReverseDivisor n ↔
      0 < n ∧ ∃ k : ℕ, 2 ≤ k ∧ Nat.reverseDigits 10 n = k * n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Section 1 (terminology).
Uses 2
Statement usesReverse divisor · Digit reversal

DefinitionProperty \(P^*\)#✓fully proved

Property \(P^*\). A natural number \(n\) has property \(P^*\) if \(n\) divides the decimal reversal of every multiple of \(n\).

def HasPropertyPStar (n : ℕ) : Prop :=
  ∀ m : ℕ, n ∣ m → n ∣ Nat.reverseDigits 10 m
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Section 2 (terminology).
Uses 1 · Used by 8
Statement usesDigit reversal
Used byUnfolding property \(P^*\) · The positive integers with property \(P^*\) are the divisors of \(99\) · Divisors of \(99\) have property \(P^*\) · For \(k \ge 2\), the number \(11 \cdot (10^k - 1)\) lacks property \(P^*\) · No reverse divisor has property \(P^*\) · Positive integers sharing a factor with \(10\) lack property \(P^*\) · Reverse divisors with quotient \(4\) lack property \(P^*\) · Palindromes with property \(P^*\)

TheoremUnfolding property \(P^*\)#✓fully proved

Unfolding property \(P^*\). A natural number \(n\) has property \(P^*\) if and only if \(n\) divides the decimal reversal of every multiple of \(n\).

theorem hasPropertyPStar_iff (n : ℕ) :
    HasPropertyPStar n ↔
      ∀ m : ℕ, n ∣ m → n ∣ Nat.reverseDigits 10 m
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Section 2 (terminology).
Uses 2
Statement usesProperty \(P^*\) · Digit reversal

TheoremThe positive integers with property \(P^*\) are the divisors of \(99\)#●ready to prove

The positive integers with property \(P^*\) are the divisors of \(99\). A natural number \(n \ge 1\) has property \(P^*\) if and only if \(n\) divides \(99\).

theorem_wanted hasPropertyPStar_iff_dvd (n : ℕ) (hn : 1 ≤ n) :
    HasPropertyPStar n ↔ n ∣ 99
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Theorem 3.
Uses 1
Statement usesProperty \(P^*\)

TheoremDivisors of \(99\) have property \(P^*\)#●ready to prove

Divisors of \(99\) have property \(P^*\). Every divisor of \(99\) has property \(P^*\).

theorem_wanted hasPropertyPStar_of_dvd (n : ℕ) (hn : n ∣ 99) :
    HasPropertyPStar n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 1.
Uses 1
Statement usesProperty \(P^*\)

TheoremPositive integers sharing a factor with \(10\) lack property \(P^*\)#●ready to prove

Positive integers sharing a factor with \(10\) lack property \(P^*\). If \(n \ge 1\) is a natural number with \(\gcd(n, 10) \ne 1\), then \(n\) does not have the property \(P^*\).

theorem_wanted not_hasPropertyPStar_of_not_coprime (n : ℕ)
    (hn : 1 ≤ n) (h : ¬ Nat.Coprime n 10) :
    ¬ HasPropertyPStar n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 2.
Uses 1
Statement usesProperty \(P^*\)

TheoremPalindromes with property \(P^*\)#●ready to prove

Palindromes with property \(P^*\). Let \(n \ge 1\) be a natural number that is a decimal palindrome, that is, whose decimal reversal equals \(n\). If \(n\) has the property \(P^*\), then \(n\) is one of \(1\), \(3\), \(9\), \(11\), \(33\) and \(99\).

theorem_wanted palindrome_hasPropertyPStar (n : ℕ) (hn : 1 ≤ n)
    (hpal : Nat.reverseDigits 10 n = n) (h : HasPropertyPStar n) :
    n = 1 ∨ n = 3 ∨ n = 9 ∨ n = 11 ∨ n = 33 ∨ n = 99
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 3.
Uses 2
Statement usesProperty \(P^*\) · Digit reversal

TheoremReverse divisors have quotient \(4\) or \(9\)#●ready to prove

If \(n\) is a reverse divisor, then the decimal reversal of \(n\) equals \(4n\) or \(9n\).

theorem_wanted reverseDigits_eq_four_or_nine_mul (n : ℕ)
    (h : IsReverseDivisor n) :
    Nat.reverseDigits 10 n = 4 * n ∨ Nat.reverseDigits 10 n = 9 * n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Theorem 1 (quoted from the literature).
Uses 2
Statement usesReverse divisor · Digit reversal

TheoremBasic reverse divisors#●ready to prove

For every natural number \(k \ge 2\), the numbers \(11(10^k - 1)\) and \(22(10^k - 1)\) both have exactly \(k + 2\) decimal digits, the decimal reversal of \(11(10^k - 1)\) equals \(9 \cdot 11(10^k - 1)\), and the decimal reversal of \(22(10^k - 1)\) equals \(4 \cdot 22(10^k - 1)\).

theorem_wanted basic_reverseDivisors (k : ℕ) (hk : 2 ≤ k) :
    (Nat.digits 10 (11 * (10 ^ k - 1))).length = k + 2 ∧
      Nat.reverseDigits 10 (11 * (10 ^ k - 1)) =
        9 * (11 * (10 ^ k - 1)) ∧
      (Nat.digits 10 (22 * (10 ^ k - 1))).length = k + 2 ∧
      Nat.reverseDigits 10 (22 * (10 ^ k - 1)) =
        4 * (22 * (10 ^ k - 1))
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Theorem 1 (quoted from the literature).
Uses 1
Statement usesDigit reversal

TheoremReverse divisors have at least four digits#●ready to prove

Every reverse divisor has at least four decimal digits.

theorem_wanted four_le_length_digits (n : ℕ)
    (h : IsReverseDivisor n) :
    4 ≤ (Nat.digits 10 n).length
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Theorem 1 (quoted from the literature).
Uses 1
Statement usesReverse divisor

TheoremReverse divisors with at most seven digits#●ready to prove

Let \(n\) be a reverse divisor with \(L\) decimal digits, where \(L \le 7\). Then \(n = 11(10^{L-2} - 1)\) or \(n = 22(10^{L-2} - 1)\), where \(L - 2\) is read as \(0\) when \(L < 2\).

theorem_wanted eq_basic_of_length_le_seven (n : ℕ)
    (h : IsReverseDivisor n)
    (h7 : (Nat.digits 10 n).length ≤ 7) :
    n = 11 * (10 ^ ((Nat.digits 10 n).length - 2) - 1) ∨
      n = 22 * (10 ^ ((Nat.digits 10 n).length - 2) - 1)
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Theorem 1 (quoted from the literature).
Uses 1
Statement usesReverse divisor

TheoremReverse divisors with quotient \(4\) lack property \(P^*\)#●ready to prove

Reverse divisors with quotient \(4\) lack property \(P^*\). If \(n > 0\) is a natural number whose decimal reversal equals \(4n\), then \(n\) does not have the property \(P^*\).

theorem_wanted not_hasPropertyPStar_of_quotient_four (n : ℕ)
    (hn : 0 < n) (h : Nat.reverseDigits 10 n = 4 * n) :
    ¬ HasPropertyPStar n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Lemma 1.
Uses 2
Statement usesProperty \(P^*\) · Digit reversal

TheoremFor \(k \ge 2\), the number \(11 \cdot (10^k - 1)\) lacks property \(P^*\)#●ready to prove

For \(k \ge 2\), the number \(11 \cdot (10^k - 1)\) lacks property \(P^*\). For every natural number \(k \ge 2\), the number \(11 \cdot (10^k - 1)\) does not have the property \(P^*\).

In the source these numbers \(1089, 10989, 109989, \dots\) are the basic reverse divisors with quotient \(9\).

theorem_wanted not_hasPropertyPStar_basic_nine (k : ℕ) (hk : 2 ≤ k) :
    ¬ HasPropertyPStar (11 * (10 ^ k - 1))
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Lemma 2.
Uses 1
Statement usesProperty \(P^*\)

TheoremNo reverse divisor has property \(P^*\)#●ready to prove

No reverse divisor has property \(P^*\). If \(n\) is a reverse divisor, then \(n\) does not have the property \(P^*\).

theorem_wanted not_hasPropertyPStar_of_isReverseDivisor (n : ℕ)
    (h : IsReverseDivisor n) :
    ¬ HasPropertyPStar n
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 4.
Uses 2
Statement usesProperty \(P^*\) · Reverse divisor

TheoremA product congruent to \(11\) modulo a power of ten#✓fully proved

For every natural number \(r\), let \(a = (10^r - 1) \cdot 100 + 89\), the integer whose decimal digits are \(r\) nines followed by \(89\), and let \(b = 10^{r+2} - 1\), the integer whose decimal digits are \(r + 2\) nines. Then the remainder of \(ab\) modulo \(10^{r+2}\) is \(11\); that is, the last \(r + 2\) decimal digits of \(ab\) are \(r\) zeros followed by \(11\).

theorem mul_nines_modEq_eleven (r : ℕ) :
    ((10 ^ r - 1) * 100 + 89) * (10 ^ (r + 2) - 1) %
        10 ^ (r + 2) = 11
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Lemma 4.

TheoremIn base \(B\), divisors of \(B^2 - 1\) divide reversals of their multiples#●ready to prove

Let \(B \ge 2\) be a natural number and let \(n\) be a natural number dividing \(B^2 - 1\). Then \(n\) divides the base-\(B\) reversal of every multiple of \(n\).

theorem_wanted dvd_reverseDigits_of_dvd (B n : ℕ) (hB : 2 ≤ B)
    (hn : n ∣ B ^ 2 - 1) (m : ℕ) (hm : n ∣ m) :
    n ∣ Nat.reverseDigits B m
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 5.
Uses 1
Statement usesDigit reversal

TheoremInfinitely many multiples with divisible reversal#●ready to prove

Let \(n\) be a natural number not divisible by \(10\), and suppose that \(n\) divides the decimal reversal of \(k_0 n\) for some natural number \(k_0 \ge 1\). Then there are infinitely many natural numbers \(k \ge 1\) such that \(n\) divides the decimal reversal of \(k n\).

theorem_wanted infinite_dvd_reverseDigits_mul (n : ℕ)
    (h10 : ¬ 10 ∣ n)
    (h : ∃ k₀ : ℕ, 1 ≤ k₀ ∧ n ∣ Nat.reverseDigits 10 (k₀ * n)) :
    Set.Infinite
      {k : ℕ | 1 ≤ k ∧ n ∣ Nat.reverseDigits 10 (k * n)}
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 6.
Uses 1
Statement usesDigit reversal

TheoremSufficient conditions for a multiple with divisible reversal#●ready to prove

Let \(n\) be a natural number such that \(\gcd(n, 10) = 1\), or \(n\) equals its decimal reversal, or \(n\) is a reverse divisor. Then there is a natural number \(k_0 \ge 1\) such that \(n\) divides the decimal reversal of \(k_0 n\).

theorem_wanted exists_dvd_reverseDigits_mul (n : ℕ)
    (h : Nat.Coprime n 10 ∨ Nat.reverseDigits 10 n = n ∨
      IsReverseDivisor n) :
    ∃ k₀ : ℕ, 1 ≤ k₀ ∧ n ∣ Nat.reverseDigits 10 (k₀ * n)
Sources
  • Mohamed Ayad and Rachid Bouchenna, "Which Integer Divides the Reverse of Any of Its Multiples?", Proposition 6.
Uses 2
Statement usesReverse divisor · Digit reversal

DefinitionComplete Young graphs#●ready to state

For natural numbers \(g\), \(k\) and \(m\), the Young graph \(Y(g, k)\) of the \(k\)-reverse multiples in base \(g\) is complete on \(m\) nodes: the nodes other than its distinguished starting node form the complete directed graph on \(m\) nodes, so \(Y(g, k)\) has \(m + 1\) nodes in all; the node \([0, 0]\) is one of these \(m\) nodes, and the starting node has an edge to every node except \([0, 0]\).

public def_wanted IsCompleteYoungGraph (g k m : Nat) : Prop
Sources
  • L. H. Kendrick, "Young Graphs: 1089 et al.", Journal of Integer Sequences 18 (2015), https://cs.uwaterloo.ca/journals/JIS/VOL18/Kendrick/ken1.tex. Definition at lines 458-460: in the source's K_m convention, the nodes other than the distinguished starting node form the complete directed graph on m nodes, so the Young graph has m + 1 total nodes including that distinguished start; [0, 0] is one of the m non-start nodes, and the starting node connects to every node except [0, 0].
Used by 1
Used byCharacterization of complete Young graphs

TheoremCharacterization of complete Young graphs#●statement formalized

Let \(g\), \(k\) and \(m\) be natural numbers with \(2 \le k < g\) and \(m \ge 2\). Then the Young graph \(Y(g, k)\) is complete on \(m\) nodes if and only if

\[\left\lfloor \frac{\gcd(g - k,\, k^2 - 1)}{k + 1} \right\rfloor = m - 1.\]
public theorem_wanted sloane_complete_young_graph_characterization
    (g k m : Nat) (hk : 2 ≤ k) (hkg : k < g) (hm : 2 ≤ m) :
    ❰IsCompleteYoungGraph❱ g k m ↔
      Nat.gcd (g - k) (k ^ 2 - 1) / (k + 1) = m - 1
Sources
  • Corollary at lines 574-576 of L. H. Kendrick, "Young Graphs: 1089 et al.", Journal of Integer Sequences 18 (2015), https://cs.uwaterloo.ca/journals/JIS/VOL18/Kendrick/ken1.tex. In the source's K_m convention, the nodes other than the distinguished starting node form the complete directed graph on m nodes, so the Young graph has m + 1 total nodes including that distinguished start; [0, 0] is one of the m non-start nodes. Natural-number division represents the source floor because all quantities are nonnegative and the denominator is positive. The hypothesis is 2 ≤ m, not 1 ≤ m. The corollary rests on a theorem whose proof starts "Since \(s_1\) exists", so it needs m - 1 ≥ 1. For m = 1 the class K_1 contains no Young graph: every Young graph is connected and contains [0, 0], so the starting node has an edge to some node other than [0, 0], while a graph in K_1 has none. With 1 ≤ m, (g, k) = (10, 9) and m = 1 give gcd(1, 80) / 10 = 0 = m - 1, but Y(10, 9) is the 1089 graph, not in K_1.
Uses 1
Statement usesComplete Young graphs
16 fully proved14 ready to prove1 statement formalized1 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.