English
A corollary of the divisibility lemma: if p divides x − y, then p divides the specified geometric sum; this yields a direct divisibility test for the sum.
Русский
Следствие леммы делимости: если p делит x−y, то делится заданная геометрическая сумма; получаем тест делимости суммы.
LaTeX
$$$p \mid (x-y) \Rightarrow p \mid \sum_{i=0}^{n-1} x^i y^{n-1-i}.$$$
Lean4
theorem sq_dvd_add_pow_sub_sub (p x : R) (n : ℕ) : p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * n - x ^ n :=
by
rcases n with - | n
· simp only [pow_zero, Nat.cast_zero, sub_zero, sub_self, dvd_zero, mul_zero]
· simp only [Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.cast_succ, add_pow, Finset.sum_range_succ, Nat.choose_self,
tsub_self, pow_one, Nat.choose_succ_self_right, pow_zero, mul_one, Nat.cast_zero, zero_add, add_tsub_cancel_left]
suffices p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by convert this; abel
apply Finset.dvd_sum
intro y hy
calc
p ^ 2 ∣ p ^ (n + 1 - y) := pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy]))
_ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) := dvd_mul_of_dvd_left (dvd_mul_left _ _) _
