Odd perfect numbers

DefinitionEulerian form of an odd perfect number#✓fully proved

For natural numbers \(N\), \(q\), \(k\) and \(n\), the quadruple \((N, q, k, n)\) is in Eulerian form when \(N\) is an odd perfect number, \(q\) is prime, \(N = q^k n^2\), \(q \equiv 1 \pmod 4\), \(k \equiv 1 \pmod 4\), and \(q\) and \(n\) are coprime.

public def EulerianForm (N q k n : ℕ) : Prop :=
  Nat.Perfect N ∧ Odd N ∧ Nat.Prime q ∧ N = q ^ k * n ^ 2 ∧
    q % 4 = 1 ∧ k % 4 = 1 ∧ Nat.Coprime q n

Used by 3

Used byRefined fifth-power bound on the Euler prime of an odd perfect number · Fifth-power bound on the Euler prime of an odd perfect number · Euler prime of an odd perfect number

DefinitionEuler prime of an odd perfect number#✓fully proved

A natural number \(q\) is an Euler prime of a natural number \(N\) when there are natural numbers \(k\) and \(n\) such that \((N, q, k, n)\) is in Eulerian form: \(N\) is an odd perfect number, \(q\) is prime, \(N = q^k n^2\), \(q \equiv 1 \pmod 4\), \(k \equiv 1 \pmod 4\), and \(q\) and \(n\) are coprime.

public def IsEulerPrime (N q : ℕ) : Prop :=
  ∃ k n, EulerianForm N q k n

Uses 1 · Used by 1

Statement usesEulerian form of an odd perfect number

Used byPrimes congruent to \(-1\) modulo \(165\) are not Euler primes

TheoremEuler's theorem on odd perfect numbers#✓fully proved

Every odd perfect number \(n\) can be written as \(n = q^s m^2\) with natural numbers \(q\), \(s\) and \(m\), where \(q\) is prime, \(q \equiv 1 \pmod 4\), \(s \equiv 1 \pmod 4\), and \(q\) and \(m\) are coprime.

The statement is conditional: whether an odd perfect number exists remains open.

public theorem euler_odd_perfect_form (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) :
    ∃ q s m : ℕ,
      q.Prime ∧ n = q ^ s * m ^ 2 ∧ Nat.ModEq 4 q 1 ∧
        Nat.ModEq 4 s 1 ∧ q.Coprime m

TheoremComparison of products of \(1 - 1/x\) under prefix-product domination#●ready to prove

Let \(k \ge 0\) and let \(z_1 \le \dots \le z_k\) and \(y_1 \le \dots \le y_k\) be real numbers, all greater than \(1\), such that \(z_1 \cdots z_l \le y_1 \cdots y_l\) for every \(l\) with \(0 \le l \le k\) (for \(l = 0\) both sides are the empty product). Then \(\prod_{i=1}^k (1 - 1/z_i) \le \prod_{i=1}^k (1 - 1/y_i)\), with equality if and only if \(z_i = y_i\) for all \(i\).

public theorem_wanted prod_one_sub_inv_le_of_prefix_prod_le (k : ℕ) (z y : Fin k → ℝ)
    (hz : Monotone z) (hy : Monotone y) (hz1 : ∀ i, 1 < z i) (hy1 : ∀ i, 1 < y i)
    (hprefix : ∀ l ≤ k, ∏ i ∈ Finset.univ.filter (fun i : Fin k => (i : ℕ) < l), z i ≤
      ∏ i ∈ Finset.univ.filter (fun i : Fin k => (i : ℕ) < l), y i) :
    ∏ i, (1 - 1 / z i) ≤ ∏ i, (1 - 1 / y i) ∧
      (∏ i, (1 - 1 / z i) = ∏ i, (1 - 1 / y i) ↔ z = y)

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 2, citing its reference [4].

TheoremFirst-element bounds for HBC-admissible tuples at \(1/2\)#●ready to prove

Let \(k \ge 1\) and let \(y_1 < y_2 < \dots < y_k\) be positive integers with \(\prod_{i=1}^{k} (1 - 1/y_i) \le 1/2 < \prod_{i=1}^{k-1} (1 - 1/y_i)\). Then \(y_1 \le k + 1\); if every \(y_i\) is odd, then \(y_1 < 2(k + 3)/3\); and if every \(y_i\) is prime, then \(y_1 < 3k/7 + 3\).

public theorem_wanted hbcAdmissible_half_first_le (k : ℕ) (hk : 0 < k) (y : Fin k → ℕ)
    (hmono : StrictMono y) (hpos : ∀ i, 0 < y i)
    (hle : ∏ i, (1 - 1 / (y i : ℚ)) ≤ 1 / 2)
    (hlt : 1 / 2 < ∏ i ∈ Finset.univ.filter (fun i : Fin k => (i : ℕ) < k - 1),
      (1 - 1 / (y i : ℚ))) :
    y ⟨0, hk⟩ ≤ k + 1 ∧
      ((∀ i, Odd (y i)) → (y ⟨0, hk⟩ : ℚ) < 2 * (k + 3) / 3) ∧
      ((∀ i, (y i).Prime) → (y ⟨0, hk⟩ : ℚ) < 3 * k / 7 + 3)

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 5.

TheoremA linear bound on the smallest prime divisor of an odd perfect number#●ready to prove

If \(N\) is an odd perfect number with \(m\) distinct prime divisors, then the smallest prime divisor \(p_1\) of \(N\) satisfies \(p_1 < 3m/7 + 3\).

public theorem_wanted oddPerfect_minFac_lt (N : ℕ) (hodd : Odd N) (hperf : N.Perfect) :
    (N.minFac : ℚ) < 3 * N.primeFactors.card / 7 + 3

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 6.

TheoremSylvester's bound on the number of prime divisors of an odd perfect number#●ready to prove

Every odd perfect number has at least five distinct prime divisors.

public theorem_wanted oddPerfect_five_le_card_primeFactors (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) : 5 ≤ N.primeFactors.card

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (ii).

TheoremDickson's finiteness theorem for odd perfect numbers#●ready to prove

For every natural number \(m\), there are only finitely many odd perfect numbers with exactly \(m\) distinct prime divisors.

public theorem_wanted finite_setOf_oddPerfect_card_primeFactors_eq (m : ℕ) :
    {N : ℕ | Odd N ∧ N.Perfect ∧ N.primeFactors.card = m}.Finite

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (iii).

TheoremSteuerwald's theorem on odd perfect numbers#●ready to prove

If \(N\) is an odd perfect number, then \(N\) has a prime divisor whose exponent in the prime factorization of \(N\) is even and different from \(2\).

public theorem_wanted oddPerfect_exists_even_factorization_ne_two (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) :
    ∃ p ∈ N.primeFactors, Even (N.factorization p) ∧ N.factorization p ≠ 2

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (iv).

TheoremMcDaniel's exponent bound for odd perfect numbers below \(10^{9118}\)#●ready to prove

If \(N\) is an odd perfect number with \(N < 10^{9118}\), then \(N\) has a prime divisor whose exponent in the prime factorization of \(N\) is at least \(6\).

public theorem_wanted oddPerfect_exists_six_le_factorization_of_lt (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) (hN : N < 10 ^ 9118) :
    ∃ p ∈ N.primeFactors, 6 ≤ N.factorization p

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (v).

TheoremOdd perfect numbers not divisible by three have at least eleven prime divisors#●ready to prove

Every odd perfect number that is not divisible by \(3\) has at least \(11\) distinct prime divisors. This is due to Kishore (1981) and Hagis (1983).

public theorem_wanted oddPerfect_eleven_le_card_primeFactors_of_not_three_dvd (N : ℕ)
    (hodd : Odd N) (hperf : N.Perfect) (h3 : ¬ 3 ∣ N) : 11 ≤ N.primeFactors.card

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (vi).

TheoremNielsen's bound on the number of prime divisors of an odd perfect number#●ready to prove

Every odd perfect number \(N\) has at least ten distinct prime divisors, and at least twelve if \(3\) does not divide \(N\).

public theorem_wanted oddPerfect_ten_le_card_primeFactors (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) :
    10 ≤ N.primeFactors.card ∧ (¬ 3 ∣ N → 12 ≤ N.primeFactors.card)

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (vii).

TheoremZelinsky's bound on the smallest prime divisor of an odd perfect number#●ready to prove

If \(N\) is an odd perfect number with \(m\) distinct prime divisors, then the smallest prime divisor \(p\) of \(N\) satisfies \(p < (m - 1)/2\).

public theorem_wanted oddPerfect_minFac_lt_card_sub_one_div_two (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) :
    (N.minFac : ℚ) < ((N.primeFactors.card : ℚ) - 1) / 2

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (viii).

TheoremOchem–Rao lower bound for odd perfect numbers#●ready to prove

Every odd perfect number exceeds \(10^{1500}\).

public theorem_wanted ten_pow_fifteen_hundred_lt_of_oddPerfect (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) : 10 ^ 1500 < N

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (ix).

TheoremGoto–Ohno–Iannucci bounds on the largest prime divisors of an odd perfect number#●ready to prove

If \(N\) is an odd perfect number, then \(N\) has three distinct prime divisors \(p\), \(q\), \(r\) with \(p \ge 10^8\), \(q \ge 10^4\) and \(r \ge 100\). Equivalently, the largest, second largest and third largest prime divisors of \(N\) are at least \(10^8\), \(10^4\) and \(100\) respectively.

public theorem_wanted oddPerfect_exists_three_large_prime_divisors (N : ℕ) (hodd : Odd N)
    (hperf : N.Perfect) :
    ∃ p ∈ N.primeFactors, ∃ q ∈ N.primeFactors, ∃ r ∈ N.primeFactors,
      p ≠ q ∧ p ≠ r ∧ q ≠ r ∧ 10 ^ 8 ≤ p ∧ 10 ^ 4 ≤ q ∧ 100 ≤ r

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 1 (x).

TheoremProduct identities for calibrating numbers#●ready to prove

Let \(a\) and \(d\) be positive integers and let \(k \ge 1\). Put \(\alpha = (a + d)/d\), and let \(n_i = 1 + \alpha^{2^{i-1}}\) for \(1 \le i < k\) and \(n_k = \alpha^{2^{k-1}}\) (the calibrating numbers for \(a/(a + d)\)). Then \(\prod_{i=1}^{k} (1 - 1/n_i) = a/(a + d)\); for every \(j\) with \(1 \le j < k\), \(\prod_{i=1}^{j} n_i = (d/a)(\alpha^{2^j} - 1)\); and \(\prod_{i=1}^{k} n_i = (d/a)(\alpha^{2^k} - \alpha^{2^{k-1}})\).

public theorem_wanted hbcCalibrating_prod_identities (a d k : ℕ) (ha : 0 < a) (hd : 0 < d)
    (hk : 1 ≤ k) :
    let α : ℚ := (a + d) / d
    let n : ℕ → ℚ := fun i => if i < k then 1 + α ^ 2 ^ (i - 1) else α ^ 2 ^ (k - 1)
    ∏ i ∈ Finset.Icc 1 k, (1 - 1 / n i) = (a : ℚ) / (a + d) ∧
      (∀ j, 1 ≤ j → j < k → ∏ i ∈ Finset.Icc 1 j, n i = (d / a) * (α ^ 2 ^ j - 1)) ∧
      ∏ i ∈ Finset.Icc 1 k, n i = (d / a) * (α ^ 2 ^ k - α ^ 2 ^ (k - 1))

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 3.

TheoremStone's product bound for HBC-admissible tuples#●ready to prove

Let \(a\) and \(d\) be coprime positive integers, let \(k \ge 1\), and let \(y_1 < y_2 < \dots < y_k\) be positive integers with \(\prod_{i=1}^{k} (1 - 1/y_i) \le a/(a + d) < \prod_{i=1}^{k-1} (1 - 1/y_i)\) (the source calls such a tuple HBC-admissible for \(a/(a + d)\)). Put \(\alpha = (a + d)/d\), let \(n_i = 1 + \alpha^{2^{i-1}}\) for \(1 \le i < k\) and \(n_k = \alpha^{2^{k-1}}\), and let \(F_k(x) = x^{2^k} - x^{2^{k-1}}\). Then some \(\kappa\) with \(1 \le \kappa \le k\) has \(\prod_{i=1}^{\kappa} y_i \le \prod_{i=1}^{\kappa} n_i\). Moreover, let \(\kappa\) with \(1 \le \kappa \le k\) satisfy this inequality while every \(\kappa'\) with \(\kappa < \kappa' \le k\) satisfies \(\prod_{i=1}^{\kappa'} n_i < \prod_{i=1}^{\kappa'} y_i\), so that \(\kappa\) is the largest such index. If \(\kappa < k\), then \(a \prod_{i=1}^{k} y_i \le F_k(\alpha d^{1/2^{\kappa}})\); if \(\kappa = k\), then \(a \prod_{i=1}^{k} y_i \le d \, F_k(\alpha)\).

public theorem_wanted hbcAdmissible_exists_prefix_le_and_prod_le (a d k : ℕ) (ha : 0 < a)
    (hd : 0 < d) (hcop : Nat.Coprime a d) (hk : 1 ≤ k) (y : ℕ → ℕ) (hy0 : 0 < y 1) (hmono : ∀ i, 1 ≤ i → i < k → y i < y (i + 1))
    (hle : ∏ i ∈ Finset.Icc 1 k, (1 - 1 / (y i : ℝ)) ≤ (a : ℝ) / (a + d))
    (hlt : (a : ℝ) / (a + d) < ∏ i ∈ Finset.Icc 1 (k - 1), (1 - 1 / (y i : ℝ))) :
    let α : ℝ := (a + d) / d
    let n : ℕ → ℝ := fun i => if i < k then 1 + α ^ 2 ^ (i - 1) else α ^ 2 ^ (k - 1)
    let ακ : ℕ → ℝ := fun κ => if κ < k then α * (d : ℝ) ^ ((1 : ℝ) / 2 ^ κ) else α
    (∃ κ ∈ Finset.Icc 1 k, ∏ i ∈ Finset.Icc 1 κ, (y i : ℝ) ≤ ∏ i ∈ Finset.Icc 1 κ, n i) ∧
      ∀ κ ∈ Finset.Icc 1 k, ∏ i ∈ Finset.Icc 1 κ, (y i : ℝ) ≤ ∏ i ∈ Finset.Icc 1 κ, n i →
        (∀ κ' ∈ Finset.Icc 1 k, κ < κ' →
          ∏ i ∈ Finset.Icc 1 κ', n i < ∏ i ∈ Finset.Icc 1 κ', (y i : ℝ)) →
        a * ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤
          (if κ = k then (d : ℝ) else 1) * (ακ κ ^ 2 ^ k - ακ κ ^ 2 ^ (k - 1))

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Theorem 1.

TheoremStone's \(\sqrt{d}\) product bound for HBC-admissible tuples#●ready to prove

Let \(a\) and \(d\) be coprime positive integers, let \(k \ge 1\), and let \(y_1 < y_2 < \dots < y_k\) be positive integers with \(\prod_{i=1}^{k} (1 - 1/y_i) \le a/(a + d) < \prod_{i=1}^{k-1} (1 - 1/y_i)\). Put \(\beta = (a + d)/\sqrt{d}\). Then \(a \prod_{i=1}^{k} y_i \le \beta^{2^k} - \beta^{2^{k-1}}\).

public theorem_wanted hbcAdmissible_prod_le_sqrt (a d k : ℕ) (ha : 0 < a) (hd : 0 < d)
    (hcop : Nat.Coprime a d) (hk : 1 ≤ k) (y : ℕ → ℕ) (hy0 : 0 < y 1) (hmono : ∀ i, 1 ≤ i → i < k → y i < y (i + 1))
    (hle : ∏ i ∈ Finset.Icc 1 k, (1 - 1 / (y i : ℝ)) ≤ (a : ℝ) / (a + d))
    (hlt : (a : ℝ) / (a + d) < ∏ i ∈ Finset.Icc 1 (k - 1), (1 - 1 / (y i : ℝ))) :
    a * ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤
      ((a + d) / Real.sqrt d) ^ 2 ^ k - ((a + d) / Real.sqrt d) ^ 2 ^ (k - 1)

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Corollary 1.

TheoremStone's \(d^{3/4}\) product bound for HBC-admissible tuples#●ready to prove

Let \(a\) and \(d\) be coprime positive integers, let \(k \ge 2\), and let \(y_1 < y_2 < \dots < y_k\) be positive integers with \(\prod_{i=1}^{k} (1 - 1/y_i) \le a/(a + d) < \prod_{i=1}^{k-1} (1 - 1/y_i)\) and \(y_1 \ne \lfloor 1 + (a + d)/d \rfloor\). Put \(\beta = (a + d)/d^{3/4}\). Then \(a \prod_{i=1}^{k} y_i \le \beta^{2^k} - \beta^{2^{k-1}}\).

public theorem_wanted hbcAdmissible_prod_le_of_ne_floor (a d k : ℕ) (ha : 0 < a) (hd : 0 < d)
    (hcop : Nat.Coprime a d) (hk : 2 ≤ k) (y : ℕ → ℕ) (hy0 : 0 < y 1) (hmono : ∀ i, 1 ≤ i → i < k → y i < y (i + 1))
    (hle : ∏ i ∈ Finset.Icc 1 k, (1 - 1 / (y i : ℝ)) ≤ (a : ℝ) / (a + d))
    (hlt : (a : ℝ) / (a + d) < ∏ i ∈ Finset.Icc 1 (k - 1), (1 - 1 / (y i : ℝ)))
    (hy1 : y 1 ≠ ⌊1 + ((a : ℝ) + d) / d⌋₊) :
    a * ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤
      ((a + d) / (d : ℝ) ^ ((3 : ℝ) / 4)) ^ 2 ^ k - ((a + d) / (d : ℝ) ^ ((3 : ℝ) / 4)) ^ 2 ^ (k - 1)

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Corollary 2.

TheoremProduct bound for HBC-admissible tuples at \(7/10\)#●ready to prove

Let \(k \ge 3\) and let \(y_1 < y_2 < \dots < y_k\) be positive integers with \(\prod_{i=1}^{k} (1 - 1/y_i) \le 7/10 < \prod_{i=1}^{k-1} (1 - 1/y_i)\). Then \(\prod_{i=1}^{k} y_i \le \frac{2}{7}\bigl(\sqrt{15}^{\,2^k} - \sqrt{15}^{\,2^{k-1}}\bigr)\).

public theorem_wanted hbcAdmissible_seven_tenths_prod_le (k : ℕ) (hk : 3 ≤ k) (y : ℕ → ℕ) (hy0 : 0 < y 1) (hmono : ∀ i, 1 ≤ i → i < k → y i < y (i + 1))
    (hle : ∏ i ∈ Finset.Icc 1 k, (1 - 1 / (y i : ℝ)) ≤ 7 / 10)
    (hlt : 7 / 10 < ∏ i ∈ Finset.Icc 1 (k - 1), (1 - 1 / (y i : ℝ))) :
    ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤
      2 / 7 * (Real.sqrt 15 ^ 2 ^ k - Real.sqrt 15 ^ 2 ^ (k - 1))

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 4.

TheoremProduct bounds for prime tuples at \(1/2\) by size of the first prime#●ready to prove

Let \(p_1 < p_2 < \dots < p_k\) be primes with \(\prod_{i=1}^{k} (1 - 1/p_i) \le 1/2 < \prod_{i=1}^{k-1} (1 - 1/p_i)\) and \(p_1 \ge 5\), and let \(F_k(x) = x^{2^k} - x^{2^{k-1}}\) and \(P = \prod_{i=1}^{k} p_i\). Then \(P \le F_k(\sqrt{8/3^{7/8}})\). Moreover, if \(6 \le p_1 < 18\), then \(P \le F_k(\sqrt{12/5^{15/16}})\); if \(18 \le p_1 < 258\), then \(P \le F_k(\sqrt{512/255^{31/32}})\); and if \(p_1 \ge 258\), then \(P \le F_k\bigl(\sqrt{2^{5/4} (2^{16} + 1)/2^{16}}\bigr)\).

public theorem_wanted hbcAdmissible_half_prime_prod_le_of_five_le (k : ℕ) (y : ℕ → ℕ) (hmono : ∀ i, 1 ≤ i → i < k → y i < y (i + 1))
    (hprime : ∀ i ∈ Finset.Icc 1 k, (y i).Prime)
    (hle : ∏ i ∈ Finset.Icc 1 k, (1 - 1 / (y i : ℝ)) ≤ 1 / 2)
    (hlt : 1 / 2 < ∏ i ∈ Finset.Icc 1 (k - 1), (1 - 1 / (y i : ℝ)))
    (h5 : 5 ≤ y 1) :
    let F : ℝ → ℝ := fun x => x ^ 2 ^ k - x ^ 2 ^ (k - 1)
    ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤ F (Real.sqrt (8 / (3 : ℝ) ^ ((7 : ℝ) / 8))) ∧
      (6 ≤ y 1 → y 1 < 18 →
        ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤ F (Real.sqrt (12 / (5 : ℝ) ^ ((15 : ℝ) / 16)))) ∧
      (18 ≤ y 1 → y 1 < 258 →
        ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤ F (Real.sqrt (512 / (255 : ℝ) ^ ((31 : ℝ) / 32)))) ∧
      (258 ≤ y 1 →
        ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤
          F (Real.sqrt ((2 : ℝ) ^ ((5 : ℝ) / 4) * (2 ^ 16 + 1) / 2 ^ 16)))

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 7.

TheoremProduct bound for prime tuples at \(1/2\) starting at \(5\)#●ready to prove

Let \(p_1 < p_2 < \dots < p_k\) be primes with \(\prod_{i=1}^{k} (1 - 1/p_i) \le 1/2 < \prod_{i=1}^{k-1} (1 - 1/p_i)\) and \(p_1 = 5\). Put \(x = \sqrt{8/3^{31/32}}\). Then \(\prod_{i=1}^{k} p_i \le x^{2^k} - x^{2^{k-1}}\).

public theorem_wanted hbcAdmissible_half_prime_prod_le_of_eq_five (k : ℕ) (y : ℕ → ℕ) (hmono : ∀ i, 1 ≤ i → i < k → y i < y (i + 1))
    (hprime : ∀ i ∈ Finset.Icc 1 k, (y i).Prime)
    (hle : ∏ i ∈ Finset.Icc 1 k, (1 - 1 / (y i : ℝ)) ≤ 1 / 2)
    (hlt : 1 / 2 < ∏ i ∈ Finset.Icc 1 (k - 1), (1 - 1 / (y i : ℝ)))
    (h5 : y 1 = 5) :
    ∏ i ∈ Finset.Icc 1 k, (y i : ℝ) ≤
      Real.sqrt (8 / (3 : ℝ) ^ ((31 : ℝ) / 32)) ^ 2 ^ k -
        Real.sqrt (8 / (3 : ℝ) ^ ((31 : ℝ) / 32)) ^ 2 ^ (k - 1)

Sources

• Andrew Stone, Improved Upper Bounds for Odd Perfect Numbers -- Part I, INTEGERS 24 (2024), Article A114, Lemma 8.

TheoremZelinsky's upper bound on the prime reciprocal sum of an odd perfect number#●ready to prove

Let \(n\) be an odd perfect number whose least prime factor \(p_1\) satisfies \(p_1 \ge 11\), and let \(T(n) = \sum_{p \mid n} 1/p\), the sum over the primes \(p\) dividing \(n\). Then \(T(n) < \log 2 - \frac{11}{50 p_1^2}\).

public theorem_wanted oddPerfect_primeReciprocalSum_lt_log_two_sub
    (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) (h11 : 11 ≤ n.minFac) :
    ∑ p ∈ n.primeFactors, (1 : ℝ) / p < Real.log 2 - 11 / (50 * (n.minFac : ℝ) ^ 2)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Corollary 1.

TheoremSurplus of an odd perfect number with least prime factor at least 11#●ready to prove

Let \(n\) be an odd perfect number whose least prime factor \(p_1\) satisfies \(p_1 \ge 11\), and let \(H(n) = \prod_{p \mid n} p/(p-1)\), the product over the primes \(p\) dividing \(n\). Then its surplus \(H(n) - 2\) satisfies \(H(n) - 2 < \frac{25}{8 p_1 \log p_1}\).

public theorem_wanted oddPerfect_abundancySup_sub_two_lt
    (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) (h11 : 11 ≤ n.minFac) :
    (abundancySup n : ℝ) - 2 < 25 / (8 * (n.minFac : ℝ) * Real.log n.minFac)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Corollary 2.

Uses 1

Statement usesProduct of \(p/(p-1)\) over the prime factors

TheoremExponential lower bound for \(1 + x + x^2\) on \((0, 1/11)\)#●ready to prove

For every real \(x\) with \(0 \le x \le 1/11\), \(\exp(x + 2x^2/5) \le 1 + x + x^2\), with equality if and only if \(x = 0\).

public theorem_wanted exp_add_two_fifths_sq_le_one_add_add_sq
    (x : ℝ) (h0 : 0 ≤ x) (h1 : x ≤ 1 / 11) :
    Real.exp (x + 2 * x ^ 2 / 5) ≤ 1 + x + x ^ 2 ∧
      (Real.exp (x + 2 * x ^ 2 / 5) = 1 + x + x ^ 2 ↔ x = 0)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 3.

TheoremLower bound for the prime-counting function at primes \(p \ge 19\)#●ready to prove

For every prime \(p \ge 19\), the number \(\pi(p)\) of primes at most \(p\) satisfies \(\pi(p) \ge p/\log p + 1\), where \(\log\) is the natural logarithm.

public theorem_wanted div_log_add_one_le_primeCounting
    (p : ℕ) (hp : p.Prime) (h19 : 19 ≤ p) :
    (p : ℝ) / Real.log p + 1 ≤ Nat.primeCounting p

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 4.

TheoremTail bound for the sum of \(1/p^2\) over primes#●ready to prove

Let \(q \ge 3\) be a prime and let \(M(q) = \sum_{p \ge q} 1/p^2\) be the sum over all primes \(p \ge q\). Then \(M(q) < \frac{1}{q \log q}\left(1 + \frac{2 \log \log q}{\log q}\right)\), where \(\log\) is the natural logarithm.

public theorem_wanted tsum_one_div_sq_primes_ge_lt
    (q : ℕ) (hq : q.Prime) (h3 : 3 ≤ q) :
    ∑' p : {p : ℕ // p.Prime ∧ q ≤ p}, (1 : ℝ) / ((p : ℕ) : ℝ) ^ 2 <
      1 / ((q : ℝ) * Real.log q) * (1 + 2 * Real.log (Real.log q) / Real.log q)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 6.

TheoremBound on the tail of the prime product of \(p^2/(p^2-1)\)#●ready to prove

Let \(q\) be an odd prime. Then \(\sum_{p \ge q} \log \frac{p^2}{p^2-1} \le \frac{1}{q \log q}\left(1 + \frac{2 \log \log q}{\log q}\right) + \frac{4}{q^3}\), where the sum runs over the primes \(p \ge q\). Equivalently, \(\log E\) is at most this bound, where \(E = \prod_{p \ge q} \frac{p^2}{p^2-1}\) is the product over the primes \(p \ge q\).

public theorem_wanted tsum_log_sq_div_sq_sub_one_primes_ge_le
    (q : ℕ) (hq : q.Prime) (hodd : Odd q) :
    ∑' p : {p : ℕ // p.Prime ∧ q ≤ p},
        Real.log (((p : ℕ) : ℝ) ^ 2 / (((p : ℕ) : ℝ) ^ 2 - 1)) ≤
      1 / ((q : ℝ) * Real.log q) * (1 + 2 * Real.log (Real.log q) / Real.log q) +
        4 / (q : ℝ) ^ 3

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 7.

TheoremUpper bound for \(\log(1 + 1/(x-1))\)#●ready to prove

For every integer \(x \ge 2\), \(\log(1 + 1/(x-1)) \le 1/x + 25/(32x^2)\), where \(\log\) is the natural logarithm.

public theorem_wanted log_one_add_one_div_sub_one_le
    (x : ℕ) (hx : 2 ≤ x) :
    Real.log (1 + 1 / ((x : ℝ) - 1)) ≤ 1 / (x : ℝ) + 25 / (32 * (x : ℝ) ^ 2)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 8.

TheoremSuryanarayana's bound for \(H(n)/h(n)\) with one odd exponent#●ready to prove

For a positive integer \(n\) write \(h(n) = \sigma(n)/n\) for its abundancy index, where \(\sigma(n)\) is the sum of the divisors of \(n\), and \(H(n) = \prod_{p \mid n} p/(p-1)\) for the product over its prime divisors. Let \(n\) be odd and let \(j\) be a prime divisor of \(n\) whose exponent in \(n\) is odd, while the exponent of every other prime divisor of \(n\) is even. Then

\[\frac{H(n)}{h(n)} \le \frac{j^2}{j^2 - 1} \prod_{p \mid n,\ p \ne j} \frac{p^3}{p^3 - 1},\]

where \(p\) runs over the prime divisors of \(n\) other than \(j\).

public theorem_wanted abundancySup_div_abundancyIndex_le_of_single_odd_exponent
    (n j : ℕ) (hn : Odd n) (hj : j ∈ n.primeFactors) (hjodd : Odd (n.factorization j))
    (heven : ∀ p ∈ n.primeFactors, p ≠ j → Even (n.factorization p)) :
    abundancySup n / abundancyIndex n ≤
      (j : ℚ) ^ 2 / ((j : ℚ) ^ 2 - 1) *
        ∏ p ∈ n.primeFactors.erase j, (p : ℚ) ^ 3 / ((p : ℚ) ^ 3 - 1)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 9.

Uses 2

Statement usesAbundancy index · Product of \(p/(p-1)\) over the prime factors

TheoremOdd perfect numbers divisible by 165 contain 5 exactly once#●ready to prove

If \(n\) is an odd perfect number divisible by \(165\), then \(5\) divides \(n\) exactly once: \(5 \mid n\) but \(25 \nmid n\).

public theorem_wanted oddPerfect_factorization_five_eq_one_of_dvd
    (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) (h165 : 165 ∣ n) :
    n.factorization 5 = 1

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 11.

TheoremBound on a prime that pushes \(\prod p/(p-1)\) past \(2\)#●ready to prove

Let \(s\) be a finite set of odd primes with \(\prod_{p \in s} p/(p-1) \le 2\), and let \(q\) be an odd prime with \(\left(\prod_{p \in s} p/(p-1)\right) \cdot q/(q-1) > 2\). Then \(q \le 2 \prod_{p \in s} (p - 1) - 1\).

public theorem_wanted le_two_mul_prod_sub_one_sub_one_of_two_lt
    (s : Finset ℕ) (hs : ∀ p ∈ s, p.Prime ∧ Odd p)
    (hle : ∏ p ∈ s, (p : ℚ) / ((p : ℚ) - 1) ≤ 2)
    (q : ℕ) (hq : q.Prime) (hqodd : Odd q)
    (hgt : 2 < (∏ p ∈ s, (p : ℚ) / ((p : ℚ) - 1)) * ((q : ℚ) / ((q : ℚ) - 1))) :
    q ≤ 2 * ∏ p ∈ s, (p - 1) - 1

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Lemma 12.

TheoremCohen–Hagis–Suryanarayana bounds on the prime reciprocal sum of an odd perfect number#●ready to prove

Let \(n\) be an odd perfect number and \(T(n) = \sum_{p \mid n} 1/p\), the sum over the primes \(p\) dividing \(n\). If \(\gcd(15, n) = 1\) then \(T(n) \le 0.693148\); if \(\gcd(15, n) = 3\) then \(T(n) \le 0.657304\); if \(\gcd(15, n) = 5\) then \(T(n) \le 0.678036\); and if \(\gcd(15, n) = 15\) then \(T(n) \le 0.673770\).

The source table also gives lower bounds, which are not stated here.

public theorem_wanted oddPerfect_primeReciprocalSum_le_of_gcd_fifteen
    (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) :
    (Nat.gcd 15 n = 1 → ∑ p ∈ n.primeFactors, (1 : ℝ) / p ≤ 0.693148) ∧
      (Nat.gcd 15 n = 3 → ∑ p ∈ n.primeFactors, (1 : ℝ) / p ≤ 0.657304) ∧
      (Nat.gcd 15 n = 5 → ∑ p ∈ n.primeFactors, (1 : ℝ) / p ≤ 0.678036) ∧
      (Nat.gcd 15 n = 15 → ∑ p ∈ n.primeFactors, (1 : ℝ) / p ≤ 0.673770)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 1, Table 1.

TheoremSuryanarayana's bounds on the prime product of an odd perfect number#●ready to prove

Let \(n\) be an odd perfect number and \(H(n) = \prod_{p \mid n} p/(p-1)\), the product over the primes \(p\) dividing \(n\). If \(\gcd(15, n) = 1\) then \(H(n) \le 2.014754\); if \(\gcd(15, n) = 3\) then \(H(n) \le 2.096234\); if \(\gcd(15, n) = 5\) then \(H(n) \le 2.031002\); and if \(\gcd(15, n) = 15\) then \(H(n) \le 2.165439\).

public theorem_wanted oddPerfect_abundancySup_le_of_gcd_fifteen
    (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) :
    (Nat.gcd 15 n = 1 → abundancySup n ≤ 2.014754) ∧
      (Nat.gcd 15 n = 3 → abundancySup n ≤ 2.096234) ∧
      (Nat.gcd 15 n = 5 → abundancySup n ≤ 2.031002) ∧
      (Nat.gcd 15 n = 15 → abundancySup n ≤ 2.165439)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 2, Table 2.

Uses 1

Statement usesProduct of \(p/(p-1)\) over the prime factors

TheoremLower bound on the prime reciprocal sum of a primitive non-deficient number#●ready to prove

Let \(n\) be a primitive non-deficient number with least prime factor \(p_1\), let \(T(n) = \sum_{p \mid n} 1/p\) and \(H(n) = \prod_{p \mid n} p/(p-1)\), with the sum and product over the primes \(p\) dividing \(n\), and let \(S = H(n) - 2\) be the surplus of \(n\). Then \(T(n) \ge \log 2 - \frac{25}{64 p_1} + \frac{S}{2} - \frac{S^2}{4}\).

public theorem_wanted primitiveNondeficient_primeReciprocalSum_ge
    (n : ℕ) (hn : IsPrimitiveNondeficient n) :
    Real.log 2 - 25 / (64 * (n.minFac : ℝ)) + ((abundancySup n : ℝ) - 2) / 2 -
        ((abundancySup n : ℝ) - 2) ^ 2 / 4 ≤
      ∑ p ∈ n.primeFactors, (1 : ℝ) / p

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 3.

Uses 2

Statement usesPrimitive non-deficient number · Product of \(p/(p-1)\) over the prime factors

TheoremUpper bound on the prime reciprocal sum of a primitive non-deficient number with one odd exponent#●ready to prove

Upper bound on the prime reciprocal sum of a primitive non-deficient number with one odd exponent. Let \(n\) be a primitive non-deficient number with least prime factor \(p_1 \ge 11\), and let \(t\) be a prime factor of \(n\) such that the exponent of \(t\) in \(n\) is odd and the exponent of every other prime factor of \(n\) is even. Suppose \(2 p_1 \le t + 2\), and let \(T(n) = \sum_{p \mid n} 1/p\), the sum over the primes \(p\) dividing \(n\). Then \(T(n) < \log 2 - \frac{11}{50 p_1^2}\).

public theorem_wanted primitiveNondeficient_primeReciprocalSum_lt_of_single_odd_exponent
    (n t : ℕ) (hn : IsPrimitiveNondeficient n) (ht : t ∈ n.primeFactors)
    (htodd : Odd (n.factorization t))
    (heven : ∀ p ∈ n.primeFactors, p ≠ t → Even (n.factorization p))
    (h11 : 11 ≤ n.minFac) (hpt : 2 * n.minFac ≤ t + 2) :
    ∑ p ∈ n.primeFactors, (1 : ℝ) / p < Real.log 2 - 11 / (50 * (n.minFac : ℝ) ^ 2)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 4.

Uses 1

Statement usesPrimitive non-deficient number

TheoremBound on the prime product of an odd perfect number via its least prime factor#●ready to prove

Let \(n\) be an odd perfect number with least prime factor \(p_1\), and let \(H(n) = \prod_{p \mid n} p/(p-1)\), the product over the primes \(p\) dividing \(n\). Then \(H(n) \le 2 + \frac{9}{4 p_1^2}\).

public theorem_wanted oddPerfect_abundancySup_le
    (n : ℕ) (hodd : Odd n) (hperf : n.Perfect) :
    abundancySup n ≤ 2 + 9 / (4 * (n.minFac : ℚ) ^ 2)

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 5.

Uses 1

Statement usesProduct of \(p/(p-1)\) over the prime factors

TheoremLower bound on the prime reciprocal sum of an odd primitive non-deficient number#●ready to prove

Let \(n\) be an odd primitive non-deficient number with least prime factor \(p_1\), let \(T(n) = \sum_{p \mid n} 1/p\) and \(H(n) = \prod_{p \mid n} p/(p-1)\), with the sum and product over the primes \(p\) dividing \(n\), and let \(S = H(n) - 2\) be the surplus of \(n\). Then \(T(n) \ge \log 2 - \frac{25}{32 p_1 \log p_1} \left(1 + \frac{2 \log \log p_1}{\log p_1}\right) + \frac{S}{2} - \frac{S^2}{4}\).

The hypothesis that \(n\) is odd is added: the statement as printed fails at \(n = 6\).

public theorem_wanted odd_primitiveNondeficient_primeReciprocalSum_ge
    (n : ℕ) (hodd : Odd n) (hn : IsPrimitiveNondeficient n) :
    Real.log 2 -
          25 / (32 * (n.minFac : ℝ) * Real.log n.minFac) *
            (1 + 2 * Real.log (Real.log n.minFac) / Real.log n.minFac) +
        ((abundancySup n : ℝ) - 2) / 2 - ((abundancySup n : ℝ) - 2) ^ 2 / 4 ≤
      ∑ p ∈ n.primeFactors, (1 : ℝ) / p

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 7.

Uses 2

Statement usesPrimitive non-deficient number · Product of \(p/(p-1)\) over the prime factors

TheoremBound on \(H(n)\) for primitive non-deficient numbers by the least prime factor#●ready to prove

For a positive integer \(n\) write \(H(n) = \prod_{p \mid n} p/(p-1)\), the product over the prime divisors of \(n\). There is a real constant \(C\) such that every primitive non-deficient number \(n\) with least prime factor \(p_1\) satisfies \(H(n) \le 2 + C/p_1\).

public theorem_wanted exists_abundancySup_le_two_add_div_minFac :
    ∃ C : ℝ, ∀ n : ℕ, IsPrimitiveNondeficient n →
      (abundancySup n : ℝ) ≤ 2 + C / n.minFac

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 8.

Uses 2

Statement usesPrimitive non-deficient number · Product of \(p/(p-1)\) over the prime factors

TheoremPrimes congruent to \(-1\) modulo \(165\) are not Euler primes#●ready to prove

For all natural numbers \(q\) and \(N\) with \(q \equiv -1 \pmod{165}\), \(q\) is not an Euler prime of \(N\). In particular, no prime \(q \equiv -1 \pmod{165}\) is the Euler prime of an odd perfect number.

public theorem_wanted not_isEulerPrime_of_mod_165_eq
    (n q : ℕ) (hq : q % 165 = 164) :
    ¬ IsEulerPrime n q

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 9.

Uses 1

Statement usesEuler prime of an odd perfect number

TheoremNo odd prime \(q\) lifts \(H\) of the odd part of \(q + 1\) across \(2\)#●ready to prove

For a positive integer \(m\) write \(H(m) = \prod_{p \mid m} p/(p-1)\), the product over the prime divisors of \(m\), and \(\operatorname{odd}(m)\) for the largest odd divisor of \(m\). There is no odd prime \(q\) with \(H(\operatorname{odd}(q+1)) < 2\) and \(H(q \cdot \operatorname{odd}(q+1)) > 2\).

For \(q = 2\) the conclusion fails: \(H(3) = 3/2 < 2\) and \(H(6) = 3 > 2\).

public theorem_wanted not_abundancySup_oddPart_succ_lt_two_and_two_lt
    (q : ℕ) (hq : q.Prime) (hodd : Odd q) :
    ¬ (abundancySup (ordCompl[2] (q + 1)) < 2 ∧
      2 < abundancySup (q * ordCompl[2] (q + 1)))

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 10.

Uses 1

Statement usesProduct of \(p/(p-1)\) over the prime factors

TheoremFifth-power bound on the Euler prime of an odd perfect number#●ready to prove

If \((n, q, e, m)\) is in Eulerian form, that is, \(n\) is an odd perfect number, \(q\) is a prime coprime to \(m\), \(n = q^e m^2\) and \(q \equiv e \equiv 1 \pmod 4\), then \(e = 1\) or \(q^5 < 2m^2\), that is, \(q < 2^{1/5} m^{2/5}\).

public theorem_wanted eulerianForm_exponent_eq_one_or_pow_five_lt
    (n q e m : ℕ) (h : EulerianForm n q e m) :
    e = 1 ∨ q ^ 5 < 2 * m ^ 2

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 11.

Uses 1

Statement usesEulerian form of an odd perfect number

TheoremRefined fifth-power bound on the Euler prime of an odd perfect number#●ready to prove

If \((n, q, e, m)\) is in Eulerian form, that is, \(n\) is an odd perfect number, \(q\) is a prime coprime to \(m\), \(n = q^e m^2\) and \(q \equiv e \equiv 1 \pmod 4\), then \(e = 1\) or \(3^2 \cdot 5^2 \cdot 11^2 \cdot 13^2 \cdot q^5 < 2m^2\), that is, \(q < \left(2/(3^2 \cdot 5^2 \cdot 11^2 \cdot 13^2)\right)^{1/5} m^{2/5}\).

public theorem_wanted eulerianForm_exponent_eq_one_or_mul_pow_five_lt
    (n q e m : ℕ) (h : EulerianForm n q e m) :
    e = 1 ∨ 3 ^ 2 * 5 ^ 2 * 11 ^ 2 * 13 ^ 2 * q ^ 5 < 2 * m ^ 2

Sources

• Joshua Zelinsky, The Sum of the Reciprocals of the Prime Divisors of an Odd Perfect or Odd Primitive Non-deficient Number, INTEGERS 25 (2025), Article A59, Proposition 12.

Uses 1

Statement usesEulerian form of an odd perfect number

3 fully proved40 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.