A prime divisor of an odd geometric sum enters either as a one residue or through a nontrivial odd order
ProvedOddPerfectNumber.geom_sum_dvd_branch_splitfactorizationnumber-theoryperfect-numbers
Let p be a prime and q a natural number with p not dividing q, and e a natural number. If p divides the sum of the first two e plus one powers of q, then either q is congruent to 1 modulo p and p divides two e plus one, or q is not congruent to 1 modulo p and the multiplicative order of q modulo p is greater than 1 and divides two e plus one.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber
theorem geom_sum_dvd_branch_split {p q e : Nat} (hp : p.Prime) (hpq : Not (Dvd.dvd p q))
(hdvd : Dvd.dvd p (∑ i ∈ Finset.range (2 * e + 1), q ^ i)) :
((q : ZMod p) = 1 ∧ Dvd.dvd p (2 * e + 1)) ∨
((q : ZMod p) ≠ 1 ∧ 1 < orderOf (q : ZMod p) ∧
Dvd.dvd (orderOf (q : ZMod p)) (2 * e + 1)) := by
sorry
end OddPerfectNumber