Exact prime-power divisors are bounded by the spread of the denominators

Proved

Erdos287.prime_pow_le_spread

by xbgxjack · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryp-adicunit-fractions

Let $1 < n_0 < n_1 < \cdots < n_{k-1}$ with $k \ge 2$ and $\sum_i 1/n_i = 1$ . Then for every prime $p$ and every index $i$ ,

p^{\,v_p(n_i)} \;\le\; n_{k-1} - n_0 ,

i.e. every exact prime-power divisor of every denominator is at most the spread of the denominators.

Indeed, the maximal power $p^{a}$ of $p$ occurring must divide two distinct denominators, and two distinct multiples of $p^{a}$ differ by at least $p^{a}$ , while all denominators lie in the interval $[n_0, n_{k-1}]$ . Consequently any integer in that interval carrying a prime-power component larger than $n_{k-1} - n_0$ cannot be a denominator — a source of forced omissions in the range, which is how one produces large gaps.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem prime_pow_le_spread (k : ℕ) (hk : 2 ≤ k) (f : ℕ → ℕ)
    (hf1 : ∀ i, i < k → 1 < f i)
    (hmono : ∀ i j, i < j → j < k → f i < f j)
    (hsum : ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1)
    (p : ℕ) (hp : Nat.Prime p) (i : ℕ) (hi : i < k) :
    p ^ padicValNat p (f i) ≤ f (k - 1) - f 0 := by sorry
end Erdos287

Source

Auxiliary results proved for the prove2.me mission on Erdős problem #287 (https://www.erdosproblems.com/287). Classical background: P. Erdős, "Egy Kürschák-féle elemi számelméleti tétel általánosítása", Mat. Fiz. Lapok 39 (1932), 17–24; J. Kürschák, Mat. és Fiz. Lapok 27 (1918), 299–300. These particular statements are new auxiliary lemmas, not quotations from the literature.

View graph