Zumkeller numbers

Definitions-Zumkeller numbers#✓fully proved

A natural number \(n\) is s-Zumkeller if its proper divisors can be split into two disjoint nonempty sets whose elements have equal sums of squares. Each of the two sums is then \((\sigma_2(n) - n^2)/2\), where \(\sigma_2(n)\) is the sum of the squares of the positive divisors of \(n\).

def IsSZumkeller (n : ℕ) : Prop :=
  ∃ A ⊆ n.properDivisors, A.Nonempty ∧ (n.properDivisors \ A).Nonempty ∧
    ∑ d ∈ A, d ^ 2 = ∑ d ∈ n.properDivisors \ A, d ^ 2
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Definition 1.
Used by 14
Used byOdd s-Zumkeller numbers divisible by \(3\) have at least eight prime factors · Harmonic mean of squared divisors of even s-Zumkeller numbers · Harmonic mean of squared divisors of s-Zumkeller numbers \(2^\alpha(2^{\alpha+1}-1)\) · Odd s-Zumkeller numbers are perfect squares · Properties of even s-Zumkeller numbers · Criterion for even s-Zumkeller numbers · \(60\) is s-Zumkeller · Lower bound for odd s-Zumkeller numbers divisible by 3 · The number 6 is not s-Zumkeller · Even s-Zumkeller numbers are divisible by 6 · Even s-Zumkeller numbers are divisible by 3 · Even s-Zumkeller numbers have at least three prime factors · Even s-Zumkeller numbers have at least twelve divisors · A prime-factor product bound for s-Zumkeller numbers

DefinitionUnitary s-Zumkeller numbers#✓fully proved

A natural number \(n\) is a unitary s-Zumkeller number when its proper unitary divisors (the unitary divisors of \(n\) other than \(n\)) split into two nonempty disjoint sets \(A\) and \(B\) with equal sums of squares, \(\sum_{d \in A} d^2 = \sum_{d \in B} d^2\).

def IsUnitarySZumkeller (n : ℕ) : Prop :=
  ∃ A ⊆ (Nat.unitaryDivisors n).erase n, A.Nonempty ∧
    ((Nat.unitaryDivisors n).erase n \ A).Nonempty ∧
    ∑ d ∈ A, d ^ 2 = ∑ d ∈ (Nat.unitaryDivisors n).erase n \ A, d ^ 2
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Definition 2.
Uses 1 · Used by 5
Statement usesUnitary divisors
Used byUnitary divisor counts of unitary s-Zumkeller numbers · Lower bounds for unitary s-Zumkeller numbers · The number 60 is unitary s-Zumkeller · No odd unitary s-Zumkeller numbers · The number 6 is not unitary s-Zumkeller

Theorem\(60\) is s-Zumkeller#✓fully proved

The number \(60\) is s-Zumkeller: the squares of its proper divisors \(1, 2, 5, 30\) sum to \(1^2 + 2^2 + 5^2 + 30^2 = 930\), which is half of the sum of the squares of all proper divisors of \(60\).

theorem isSZumkeller_sixty : IsSZumkeller 60
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Example 1.
Uses 1
Statement usess-Zumkeller numbers

TheoremThe number 6 is not s-Zumkeller#✓fully proved

The number \(6\) is not an s-Zumkeller number: the squares of its proper divisors sum to \(1^2 + 2^2 + 3^2 = 14\), and they admit no split into two parts with equal sums.

theorem not_isSZumkeller_six : ¬ IsSZumkeller 6
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Section 1.
Uses 1
Statement usess-Zumkeller numbers

TheoremThe number 60 is unitary s-Zumkeller#✓fully proved

The number \(60\) is a unitary s-Zumkeller number: its proper unitary divisors are \(1, 3, 4, 5, 12, 15, 20\), and \(20^2 + 3^2 + 1^2 = 410\) is half the sum of their squares.

theorem isUnitarySZumkeller_sixty : IsUnitarySZumkeller 60
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Example 2.
Uses 2
Statement usesUnitary s-Zumkeller numbers
Proof usesUnitary divisors

TheoremThe number 6 is not unitary s-Zumkeller#✓fully proved

The number \(6\) is not a unitary s-Zumkeller number.

theorem not_isUnitarySZumkeller_six : ¬ IsUnitarySZumkeller 6
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Section 1.
Uses 2
Statement usesUnitary s-Zumkeller numbers
Proof usesUnitary divisors

TheoremProduct formulas for the sum of divisors#●ready to prove

Let \(n \ne 0\) be a natural number, let \(\sigma(n)\) be the sum of the divisors of \(n\), and for each prime \(p\) dividing \(n\) let \(k_p\) be the exponent of \(p\) in \(n\). Then, with products over the primes \(p\) dividing \(n\),

\[\sigma(n) = \prod_{p \mid n} \frac{p^{k_p + 1} - 1}{p - 1}\]

and

\[\frac{\sigma(n)}{n} = \prod_{p \mid n} \frac{p^{k_p + 1} - 1}{p^{k_p} (p - 1)}.\]

If moreover \(n > 1\), then \(\sigma(n)/n < \prod_{p \mid n} p/(p - 1)\).

public theorem_wanted sigma_one_prod_formulas (n : ℕ) (hn : n ≠ 0) :
    (ArithmeticFunction.sigma 1 n : ℚ) =
        ∏ p ∈ n.primeFactors, ((p : ℚ) ^ (n.factorization p + 1) - 1) / (p - 1) ∧
      (ArithmeticFunction.sigma 1 n : ℚ) / n =
        ∏ p ∈ n.primeFactors,
          ((p : ℚ) ^ (n.factorization p + 1) - 1) / ((p : ℚ) ^ n.factorization p * (p - 1)) ∧
      (1 < n → (ArithmeticFunction.sigma 1 n : ℚ) / n < ∏ p ∈ n.primeFactors, (p : ℚ) / (p - 1))
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Lemma 1(i) (quoting Peng and Bhaskara Rao).

TheoremProduct formulas for the sum of squared divisors#●ready to prove

Let \(n \ne 0\) be a natural number, let \(\sigma_2(n)\) be the sum of the squares of the divisors of \(n\), and for each prime \(p\) dividing \(n\) let \(k_p\) be the exponent of \(p\) in \(n\). Then, with products over the primes \(p\) dividing \(n\),

\[\sigma_2(n) = \prod_{p \mid n} \frac{p^{2(k_p + 1)} - 1}{p^2 - 1}\]

and

\[\frac{\sigma_2(n)}{n^2} = \prod_{p \mid n} \frac{p^{2(k_p + 1)} - 1}{p^{2k_p} (p^2 - 1)}.\]

If moreover \(n > 1\), then \(\sigma_2(n)/n^2 < \prod_{p \mid n} p^2/(p^2 - 1)\).

public theorem_wanted sigma_two_prod_formulas (n : ℕ) (hn : n ≠ 0) :
    (ArithmeticFunction.sigma 2 n : ℚ) =
        ∏ p ∈ n.primeFactors, ((p : ℚ) ^ (2 * (n.factorization p + 1)) - 1) / (p ^ 2 - 1) ∧
      (ArithmeticFunction.sigma 2 n : ℚ) / n ^ 2 =
        ∏ p ∈ n.primeFactors,
          ((p : ℚ) ^ (2 * (n.factorization p + 1)) - 1) /
            ((p : ℚ) ^ (2 * n.factorization p) * (p ^ 2 - 1)) ∧
      (1 < n → (ArithmeticFunction.sigma 2 n : ℚ) / n ^ 2 <
        ∏ p ∈ n.primeFactors, (p : ℚ) ^ 2 / (p ^ 2 - 1))
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Lemma 1(ii) (quoting Peng and Bhaskara Rao).

TheoremNumber of unitary divisors#●ready to prove

A positive integer \(n\) with \(m\) distinct prime factors has exactly \(2^m\) unitary divisors.

public theorem_wanted card_unitaryDivisors (n : ℕ) (hn : n ≠ 0) :
    (Nat.unitaryDivisors n).card = 2 ^ n.primeFactors.card
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Lemma 2 (quoting Bege).
Uses 1
Statement usesUnitary divisors

TheoremSum of squares of unitary divisors#●ready to prove

For every positive integer \(n\), the sum of the squares of the unitary divisors of \(n\) equals \(\prod_{p} \left(1 + p^{2k_p}\right)\), where \(p\) ranges over the distinct prime factors of \(n\) and \(k_p\) is the exponent of \(p\) in \(n\).

public theorem_wanted sum_sq_unitaryDivisors (n : ℕ) (hn : n ≠ 0) :
    ∑ d ∈ Nat.unitaryDivisors n, d ^ 2 =
      ∏ p ∈ n.primeFactors, (1 + p ^ (2 * n.factorization p))
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Lemma 3(i) (quoting Subbarao and Warren).
Uses 1
Statement usesUnitary divisors

TheoremProperties of even s-Zumkeller numbers#●ready to prove

Let \(n\) be an even s-Zumkeller number and let \(\sigma_2(n)\) be the sum of the squares of the positive divisors of \(n\). Then \(\sigma_2(n)\) is even, some odd prime \(p\) divides \(n\) with an odd exponent in the prime factorization of \(n\), and \(3n^2 \le 2\sigma_2(n)\).

public theorem_wanted isSZumkeller_even_props (n : ℕ) (h : IsSZumkeller n) (he : Even n) :
    Even (ArithmeticFunction.sigma 2 n) ∧
      (∃ p ∈ n.primeFactors, Odd p ∧ Odd (n.factorization p)) ∧
      3 * n ^ 2 ≤ 2 * ArithmeticFunction.sigma 2 n
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 1.
Uses 1
Statement usess-Zumkeller numbers

TheoremCriterion for even s-Zumkeller numbers#●ready to prove

Let \(n\) be an even positive integer and let \(\sigma_2(n)\) be the sum of the squares of the positive divisors of \(n\). Then \(n\) is s-Zumkeller if and only if there is a (possibly empty) set \(S\) of proper divisors of \(n\), not containing \(n/2\), such that \(4 \sum_{d \in S} d^2 = 2\sigma_2(n) - 3n^2\).

public theorem_wanted isSZumkeller_iff_of_even (n : ℕ) (hn : 0 < n) (he : Even n) :
    IsSZumkeller n ↔
      ∃ S ⊆ n.properDivisors.erase (n / 2),
        4 * (∑ d ∈ S, d ^ 2 : ℤ) = 2 * ArithmeticFunction.sigma 2 n - 3 * n ^ 2
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 2.
Uses 1
Statement usess-Zumkeller numbers

TheoremEven s-Zumkeller numbers have at least twelve divisors#●ready to prove

If \(n\) is an even s-Zumkeller number, then \(n\) has at least \(12\) positive divisors.

public theorem_wanted twelve_le_card_divisors_of_isSZumkeller (n : ℕ) (h : IsSZumkeller n)
    (he : Even n) : 12 ≤ n.divisors.card
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 3.
Uses 1
Statement usess-Zumkeller numbers

TheoremEven s-Zumkeller numbers are divisible by 3#●ready to prove

If \(n\) is an even s-Zumkeller number, then \(3\) divides \(n\).

public theorem_wanted three_dvd_of_isSZumkeller (n : ℕ) (h : IsSZumkeller n) (he : Even n) :
    3 ∣ n
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 4.
Uses 1
Statement usess-Zumkeller numbers

TheoremEven s-Zumkeller numbers are divisible by 6#●ready to prove

Every even s-Zumkeller number is divisible by \(6\).

public theorem_wanted six_dvd_of_isSZumkeller (n : ℕ) (h : IsSZumkeller n) (he : Even n) :
    6 ∣ n
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Corollary 1.
Uses 1
Statement usess-Zumkeller numbers

TheoremA prime-factor product bound for s-Zumkeller numbers#●ready to prove

Let \(n\) be an s-Zumkeller number and let \(p_1\) be its least prime factor. Then

\[\frac{2}{p_1^2} + 1 < \prod_{p} \frac{p^2}{p^2 - 1},\]

where the product ranges over the distinct prime factors \(p\) of \(n\).

public theorem_wanted two_div_minFac_sq_add_one_lt_prod (n : ℕ) (h : IsSZumkeller n) :
    2 / (n.minFac : ℚ) ^ 2 + 1 < ∏ p ∈ n.primeFactors, (p : ℚ) ^ 2 / (p ^ 2 - 1)
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 5.
Uses 1
Statement usess-Zumkeller numbers

TheoremEven s-Zumkeller numbers have at least three prime factors#●ready to prove

If \(n\) is an even s-Zumkeller number, then \(n\) has at least \(3\) distinct prime factors.

public theorem_wanted three_le_card_primeFactors_of_isSZumkeller_even (n : ℕ)
    (h : IsSZumkeller n) (he : Even n) : 3 ≤ n.primeFactors.card
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 6(i).
Uses 1
Statement usess-Zumkeller numbers

TheoremOdd s-Zumkeller numbers divisible by \(3\) have at least eight prime factors#●ready to prove

Every odd s-Zumkeller number divisible by \(3\) has at least \(8\) distinct prime factors.

public theorem_wanted eight_le_card_primeFactors_of_isSZumkeller_odd (n : ℕ)
    (h : IsSZumkeller n) (ho : Odd n) (h3 : 3 ∣ n) : 8 ≤ n.primeFactors.card
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 6(ii).
Uses 1
Statement usess-Zumkeller numbers

TheoremOdd s-Zumkeller numbers are perfect squares#●ready to prove

Every odd s-Zumkeller number is a perfect square.

public theorem_wanted isSquare_of_isSZumkeller_odd (n : ℕ) (h : IsSZumkeller n) (ho : Odd n) :
    IsSquare n
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 7.
Uses 1
Statement usess-Zumkeller numbers

TheoremLower bound for odd s-Zumkeller numbers divisible by 3#●ready to prove

Every odd s-Zumkeller number \(n\) divisible by \(3\) satisfies \(n \ge 12442607161209225 = (3 \cdot 5 \cdot 7 \cdot 11 \cdot 13 \cdot 17 \cdot 19 \cdot 23)^2\).

public theorem_wanted le_of_isSZumkeller_odd_three_dvd (n : ℕ) (h : IsSZumkeller n)
    (ho : Odd n) (h3 : 3 ∣ n) : 12442607161209225 ≤ n
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 8.
Uses 1
Statement usess-Zumkeller numbers

TheoremHarmonic mean of squared divisors of even s-Zumkeller numbers#●ready to prove

Let \(n\) be an even s-Zumkeller number and let \(\tau(n)\) be the number of positive divisors of \(n\). Then \(\tau(n) / \sum_{d \mid n} d^{-2} \le 2\tau(n)/3\), where the sum runs over the positive divisors \(d\) of \(n\).

public theorem_wanted harmonicMeanSq_le_of_isSZumkeller (n : ℕ) (h : IsSZumkeller n)
    (he : Even n) :
    (n.divisors.card : ℚ) / ∑ d ∈ n.divisors, 1 / (d : ℚ) ^ 2 ≤ 2 * n.divisors.card / 3
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 9.
Uses 1
Statement usess-Zumkeller numbers

TheoremHarmonic mean of squared divisors of s-Zumkeller numbers \(2^\alpha(2^{\alpha+1}-1)\)#●ready to prove

Let \(\alpha \ge 1\) be an integer, let \(n = 2^\alpha (2^{\alpha+1} - 1)\) and let \(\tau(n)\) be the number of positive divisors of \(n\). If \(n\) is s-Zumkeller, then \(\tau(n) / \sum_{d \mid n} d^{-2} < 2^{2\alpha+3}/3\), where the sum runs over the positive divisors \(d\) of \(n\).

public theorem_wanted harmonicMeanSq_lt_of_isSZumkeller_mersenne (α n : ℕ) (hα : 1 ≤ α)
    (hn : n = 2 ^ α * (2 ^ (α + 1) - 1)) (h : IsSZumkeller n) :
    (n.divisors.card : ℚ) / ∑ d ∈ n.divisors, 1 / (d : ℚ) ^ 2 < 2 ^ (2 * α + 3) / 3
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 10.
Uses 1
Statement usess-Zumkeller numbers

TheoremLower bounds for unitary s-Zumkeller numbers#●ready to prove

Let \(n\) be a unitary s-Zumkeller number, let \(q\) be the least unitary divisor of \(n\) greater than \(1\), and for each prime \(p\) dividing \(n\) let \(k_p\) be the exponent of \(p\) in \(n\). Then, with both sums over all unitary divisors \(d\) of \(n\) (including \(n\) itself), \(n^2 (2/q^2 + 1) \le \sum_d d^2\) and \(2/q^2 + 1 \le \sum_d 1/d^2\). Moreover \(2/q^2 + 1 \le \prod_{p \mid n} (1 + p^{2k_p})/p^{2k_p}\), the product running over the primes \(p\) dividing \(n\).

The number \(q\) is the smallest of the prime powers \(p^{k_p}\).

public theorem_wanted isUnitarySZumkeller_bounds (n q : ℕ) (h : IsUnitarySZumkeller n)
    (hq : IsLeast {d | d ∈ Nat.unitaryDivisors n ∧ 1 < d} q) :
    (n : ℚ) ^ 2 * (2 / (q : ℚ) ^ 2 + 1) ≤ ∑ d ∈ Nat.unitaryDivisors n, (d : ℚ) ^ 2 ∧
      2 / (q : ℚ) ^ 2 + 1 ≤ ∑ d ∈ Nat.unitaryDivisors n, 1 / (d : ℚ) ^ 2 ∧
      2 / (q : ℚ) ^ 2 + 1 ≤
        ∏ p ∈ n.primeFactors,
          (1 + ((p : ℚ) ^ n.factorization p) ^ 2) / ((p : ℚ) ^ n.factorization p) ^ 2
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 11.
Uses 2
Statement usesUnitary s-Zumkeller numbers · Unitary divisors

TheoremUnitary divisor counts of unitary s-Zumkeller numbers#●ready to prove

Let \(n\) be a unitary s-Zumkeller number and let \(q\) be the least unitary divisor of \(n\) greater than \(1\). If \(q = 2\), then \(n\) has more than \(2^6\) unitary divisors; if \(q = 3\) or \(q = 4\), then \(n\) has more than \(2^2\) unitary divisors.

public theorem_wanted card_unitaryDivisors_of_isUnitarySZumkeller (n q : ℕ)
    (h : IsUnitarySZumkeller n) (hq : IsLeast {d | d ∈ Nat.unitaryDivisors n ∧ 1 < d} q) :
    (q = 2 → 2 ^ 6 < (Nat.unitaryDivisors n).card) ∧
      (q = 3 → 2 ^ 2 < (Nat.unitaryDivisors n).card) ∧
      (q = 4 → 2 ^ 2 < (Nat.unitaryDivisors n).card)
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 12.
Uses 2
Statement usesUnitary s-Zumkeller numbers · Unitary divisors

TheoremNo odd unitary s-Zumkeller numbers#●ready to prove

There is no odd unitary s-Zumkeller number.

public theorem_wanted not_isUnitarySZumkeller_of_odd (n : ℕ) (ho : Odd n) :
    ¬ IsUnitarySZumkeller n
Sources
  • Jayanta Kalita and Helen K. Saikia, A Study on Generalized Zumkeller Numbers, INTEGERS 24 (2024), Article A95, Proposition 13.
Uses 1
Statement usesUnitary s-Zumkeller numbers

DefinitionProduct of the divisors#✓fully proved

For a natural number \(n\), \(T(n)\) is the product of all positive divisors of \(n\). For \(n = 0\) the set of divisors is taken to be empty, so \(T(0) = 1\).

def divisorProd (n : ℕ) : ℕ := ∏ d ∈ n.divisors, d
Used by 4
Used bySquare of the product of the divisors · \(k\)-m-perfect numbers · Super-m-Zumkeller numbers · Criterion for super-m-Zumkeller numbers

DefinitionSuper-m-Zumkeller numbers#✓fully proved

For a natural number \(n\), let \(T(n)\) be the product of the positive divisors of \(n\) (for \(n = 0\) the divisor set is taken to be empty, so \(T(0) = 1\)). Then \(n\) is super-m-Zumkeller if there is a set \(A\) of positive divisors of \(T(n)\) such that the product of the elements of \(A\) equals the product of the positive divisors of \(T(n)\) that are not in \(A\); that is, the divisors of \(T(n)\) split into two complementary sets, one of which may be empty, with equal products.

def IsSuperMZumkeller (n : ℕ) : Prop :=
  ∃ A : Finset ℕ, A ⊆ (divisorProd n).divisors ∧
    (∏ d ∈ A, d) = ∏ d ∈ (divisorProd n).divisors \ A, d
Uses 1 · Used by 8
Statement usesProduct of the divisors
Used by\(4\) is super-m-Zumkeller but not \(k\)-m-perfect for \(k \ge 2\) · Criterion for super-m-Zumkeller numbers · \(k\)-m-perfect numbers with \(k\) a positive multiple of \(4\) are super-m-Zumkeller · Super-m-Zumkeller prime powers · Products of at least three distinct primes are super-m-Zumkeller · Powers of \(2\) times at least three distinct odd primes are super-m-Zumkeller · Odd powers of \(2\) times two distinct odd primes are super-m-Zumkeller · Super-m-Zumkeller numbers \(n \ge 2\) have at least three divisors

Definition\(k\)-m-perfect numbers#✓fully proved

For natural numbers \(k\) and \(n\), \(n\) is \(k\)-m-perfect if \(T(n) = n^k\), where \(T(n)\) is the product of the divisors of \(n\).

def IsKMPerfect (k n : ℕ) : Prop := divisorProd n = n ^ k
Uses 1 · Used by 2
Statement usesProduct of the divisors
Used by\(4\) is super-m-Zumkeller but not \(k\)-m-perfect for \(k \ge 2\) · \(k\)-m-perfect numbers with \(k\) a positive multiple of \(4\) are super-m-Zumkeller

TheoremSquare of the product of the divisors#●ready to prove

For every positive integer \(n\), let \(T(n)\) be the product of the positive divisors of \(n\) and \(\tau(n)\) their number. Then \(T(n)^2 = n^{\tau(n)}\).

The paper writes this as \(T(n) = n^{\tau(n)/2}\).

theorem_wanted divisorProd_sq (n : ℕ) (hn : 0 < n) :
    (divisorProd n) ^ 2 = n ^ (n.divisors.card)
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Lemma 1.
Uses 1
Statement usesProduct of the divisors

TheoremSuper-m-Zumkeller numbers \(n \ge 2\) have at least three divisors#●ready to prove

If a natural number \(n \ge 2\) is super-m-Zumkeller, then the number \(\tau(n)\) of positive divisors of \(n\) satisfies \(\tau(n) \ge 3\).

theorem_wanted three_le_card_divisors_of_isSuperMZumkeller (n : ℕ)
    (hn : 2 ≤ n) (h : IsSuperMZumkeller n) :
    3 ≤ n.divisors.card
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Theorem 1.
Uses 1
Statement usesSuper-m-Zumkeller numbers

TheoremCriterion for super-m-Zumkeller numbers#●ready to prove

Let \(n \ge 2\) be an integer, let \(\tau(n)\) be the number of positive divisors of \(n\) and \(T(n)\) their product. Then \(n\) is super-m-Zumkeller if and only if \(8\) divides \(\alpha \cdot \tau(n) \cdot \tau(T(n))\) for every prime \(p\) dividing \(n\), where \(\alpha\) is the exponent of \(p\) in \(n\).

theorem_wanted isSuperMZumkeller_iff (n : ℕ) (hn : 2 ≤ n) :
    IsSuperMZumkeller n ↔
      ∀ p ∈ n.primeFactors,
        8 ∣ (n.factorization p) * n.divisors.card *
          (divisorProd n).divisors.card
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Theorem 2.
Uses 2
Statement usesSuper-m-Zumkeller numbers · Product of the divisors

TheoremSuper-m-Zumkeller prime powers#●ready to prove

Let \(p\) be a prime and \(\alpha \ge 1\) an integer. Then \(p^\alpha\) is super-m-Zumkeller if and only if \(\alpha \equiv 0, 2, 5, 7, 8, 10, 13\) or \(15 \pmod{16}\).

theorem_wanted isSuperMZumkeller_prime_pow_iff (p : ℕ)
    (hp : p.Prime) (a : ℕ) (ha : 1 ≤ a) :
    IsSuperMZumkeller (p ^ a) ↔
      a % 16 ∈ ({0, 2, 5, 7, 8, 10, 13, 15} : Finset ℕ)
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Theorem 3.
Uses 1
Statement usesSuper-m-Zumkeller numbers

TheoremProducts of at least three distinct primes are super-m-Zumkeller#●ready to prove

For every finite set \(S\) of at least three primes, the product \(\prod_{p \in S} p\) is super-m-Zumkeller.

theorem_wanted isSuperMZumkeller_prod_primes (s : Finset ℕ)
    (hs : ∀ p ∈ s, p.Prime) (hcard : 3 ≤ s.card) :
    IsSuperMZumkeller (∏ p ∈ s, p)
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Corollary 1.
Uses 1
Statement usesSuper-m-Zumkeller numbers

TheoremOdd powers of \(2\) times two distinct odd primes are super-m-Zumkeller#●ready to prove

Let \(k\) be an odd natural number and let \(p\) and \(q\) be distinct odd primes. Then \(2^k p q\) is super-m-Zumkeller.

The primes are required to be odd because the paper's proof uses that this number has \((k+1) \cdot 2^2\) divisors.

theorem_wanted isSuperMZumkeller_two_pow_mul_two_primes (k : ℕ)
    (hk : Odd k) (p q : ℕ) (hp : p.Prime) (hq : q.Prime)
    (hp2 : p ≠ 2) (hq2 : q ≠ 2) (hpq : p ≠ q) :
    IsSuperMZumkeller ((2 : ℕ) ^ k * (p * q))
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Corollary 2.
Uses 1
Statement usesSuper-m-Zumkeller numbers

TheoremPowers of \(2\) times at least three distinct odd primes are super-m-Zumkeller#●ready to prove

Let \(k\) be a natural number and \(S\) a finite set of at least three odd primes. Then \(2^k \prod_{p \in S} p\) is super-m-Zumkeller.

The primes are required to be odd because the paper's proof uses that this number has \((k+1)2^r\) divisors, where \(r\) is the number of primes in \(S\).

theorem_wanted isSuperMZumkeller_two_pow_mul_prod_primes (k : ℕ)
    (s : Finset ℕ) (hs : ∀ p ∈ s, p.Prime) (hs2 : 2 ∉ s)
    (hcard : 3 ≤ s.card) :
    IsSuperMZumkeller ((2 : ℕ) ^ k * ∏ p ∈ s, p)
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Corollary 2.
Uses 1
Statement usesSuper-m-Zumkeller numbers

Theorem\(k\)-m-perfect numbers with \(k\) a positive multiple of \(4\) are super-m-Zumkeller#●ready to prove

Let \(k \ge 2\) be a natural number with \(k \equiv 0 \pmod 4\). Then every natural number that is \(k\)-m-perfect is super-m-Zumkeller.

theorem_wanted isSuperMZumkeller_of_isKMPerfect (k n : ℕ)
    (hk : 2 ≤ k) (hk4 : k % 4 = 0) (h : IsKMPerfect k n) :
    IsSuperMZumkeller n
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Theorem 6.
Uses 2
Statement uses\(k\)-m-perfect numbers · Super-m-Zumkeller numbers

Theorem\(4\) is super-m-Zumkeller but not \(k\)-m-perfect for \(k \ge 2\)#●ready to prove

The number \(4\) is super-m-Zumkeller, and for no natural number \(k \ge 2\) is \(4\) a \(k\)-m-perfect number. This is the paper's counterexample to the converse of Theorem 6.

theorem_wanted isSuperMZumkeller_four_not_kmPerfect :
    IsSuperMZumkeller 4 ∧ ∀ k : ℕ, 2 ≤ k → ¬ IsKMPerfect k 4
Sources
  • Harish Patodia, "Super m-Zumkeller Numbers", Theorem 6.
Uses 2
Statement uses\(k\)-m-perfect numbers · Super-m-Zumkeller numbers
9 fully proved28 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.