Wolstenholme's theorem

For a prime p ≥ 5: the harmonic sum Σ_{k=1}^{p-1} 1/k vanishes in ZMod (p²), and C(2p - 1, p - 1) ≡ 1 (mod p³), C(2p, p) ≡ 2 (mod p³) (Wolstenholme, 1862). The harmonic lemma pairs k with p - k, giving 2H = -p Σ 1/k², and Σ 1/k² ≡ Σ k² ≡ 0 (mod p) because inversion permutes the units of ZMod p. For the binomial, (p - 1)! · C(2p - 1, p - 1) = Π (p + k) is expanded in ZMod (p³) as (p - 1)! (1 + pS + p²(S² - Q)/2) with S ≡ 0 (mod p²) and Q ≡ 0 (mod p).

Main results

• Wolstenholme.harmonic_sum_eq_zero: sum of 1/k for k < p vanishes in ZMod (p^2), p >= 5 prime
• Wolstenholme.choose_modEq: C(2p-1, p-1) = 1 and C(2p, p) = 2 mod p^3 for primes p >= 5

References

• J. Wolstenholme, On certain properties of prime numbers, Quart. J. Pure Appl. Math. 5 (1862), 35–39.
• The harmonic form (mod p²) is also in facebookresearch/atlas-lean, MathlibExt.NumberTheory.Wolstenholme.wolstenholme; the proof here is independent.

theorem Wolstenholme.harmonic_sum_eq_zero (p : ℕ) (hp : Nat.Prime p) (h5 : 5 ≤ p) : ∑ i ∈ Finset.range (p - 1), (↑(i + 1))⁻¹ = 0

Wolstenholme's harmonic lemma. For a prime p ≥ 5, ∑_{k=1}^{p-1} 1/k = 0 in ℤ/p².

theorem Wolstenholme.choose_modEq (p : ℕ) (hp : Nat.Prime p) (h5 : 5 ≤ p) : (2 * p - 1).choose (p - 1) ≡ 1 [MOD p ^ 3] ∧ (2 * p).choose p ≡ 2 [MOD p ^ 3]

Wolstenholme's theorem (1862). For a prime p ≥ 5, C(2p - 1, p - 1) ≡ 1 (mod p³); equivalently C(2p, p) ≡ 2 (mod p³).