A soluble congruence class modulo four hundred thirty-nine with distinct denominators

Proved

ErdosStraus242.family_mod439

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

egyptian-fractionsnumber-theory

For every natural number $n>2$ with $n\bmod439=419$ , there are natural numbers $1\le x<y<z$ with $4/n=1/x+1/y+1/z$ in $\mathbb Q$ .

For $n=439k+419$ , take $(5(22k+21),110n,110(22k+21)n)$ . This is an explicit specialization of the Bloom–Elsholtz parametrization on p. 239 with $(a,c,d)=(1,22,5)$ , for which $c n+a=22(439k+419)+1=439(22k+21)$ , so $b=22k+21$ and the identity $4/n=1/(abd)+1/(acdn)+1/(bcdn)$ holds with denominators $5(22k+21)$ , $110n$ and $110(22k+21)n$ . The three denominators are positive, distinct and strictly ordered for every $k\ge0$ , including the smallest input $n=419$ . This family adds a further congruence sieve within the mission six residual classes modulo $840$ : the residue $419$ modulo $439$ survives the earlier mod-11, mod-19, mod-23, mod-31, mod-43, mod-47, mod-59, mod-71, mod-83, mod-107, mod-131, mod-139, mod-151, mod-163, mod-167, mod-179, mod-191, mod-199, mod-211, mod-223, mod-227, mod-239, mod-251, mod-263, mod-271, mod-283, mod-307, mod-311, mod-331, mod-347, mod-359, mod-367, mod-379, mod-383, mod-419 and mod-431 sieves.

Preamble

import Definitions.Def_ErdosStraus242
import Mathlib.Data.Finset.Insert
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Push
import Mathlib.Tactic.Ring

Formal statement

namespace ErdosStraus242
theorem family_mod439 (n : ℕ) (hn : 2 < n)
    (hmod : n % 439 ∈ ({419} : Finset ℕ)) :
    IsErdosStraus n := by sorry
end ErdosStraus242

Source

Bloom and Elsholtz, Egyptian fractions, Nieuw Archief voor Wiskunde 5/23 no. 4 (2022), p. 239, the displayed identity following c*n+a=(4*a*c*d-1)*b: 4/n=1/(a*b*d)+1/(a*c*d*n)+1/(b*c*d*n). https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf. Specialize (a,c,d) to (1,22,5); the source identity is retained exactly.

View graph