English
If p is prime and p divides x − y, and p does not divide x or n, then p does not divide the geometric sum ∑_{i=0}^{n-1} x^i y^{n-1−i}. This is a partial non-divisibility result.
Русский
Если p — простое число и p делит x−y, причём p не делит ни x, ни n, то p не делит геометрическую сумму ∑ x^i y^{n−1−i}. Это частный результат не делимости.
LaTeX
$$$\text{Prime}(p) \rightarrow (p \nmid x) \land (p \nmid n) \Rightarrow p \nmid \sum_{i=0}^{n-1} x^i y^{n-1-i}.$$$
Lean4
theorem not_dvd_geom_sum₂ {p : R} (hp : Prime p) (hxy : p ∣ x - y) (hx : ¬p ∣ x) (hn : ¬p ∣ n) :
¬p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) := fun h =>
hx <| hp.dvd_of_dvd_pow <| (hp.dvd_or_dvd <| (dvd_geom_sum₂_iff_of_dvd_sub' hxy).mp h).resolve_left hn
