English
Let p be an odd prime, with x<y or y<x as required; if p ∣ x − y and p ∤ x, then for any nonzero and even n, padicValNat p (x^n − y^n) equals padicValNat p (x − y) plus padicValNat p n.
Русский
Пусть p — нечётная простая. При условии p|x−y, p∤x и n>0 с чётной четностью, выполняется: v_p(x^n − y^n) = v_p(x − y) + v_p(n).
LaTeX
$$$\\forall x,y \\in \\mathbb{N},\\ p \\text{ нечётная простая},\\ x>y,\\ p \\mid (x-y),\\ p \\nmid x,\\ Ne n 0,\\ n\\text{ чётно} \\Rightarrow \\mathrm{padicVal}_p(x^n - y^n) = \\mathrm{padicVal}_p(x - y) + \\mathrm{padicVal}_p(n)$$$
Lean4
theorem pow_sub_pow (hyx : y < x) (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : n ≠ 0) :
padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n :=
by
rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
iterate 3 rw [padicValNat_eq_emultiplicity]
· exact Nat.emultiplicity_pow_sub_pow hp.out hp1 hxy hx n
· exact hn
· exact Nat.sub_ne_zero_of_lt hyx
· exact Nat.sub_ne_zero_of_lt (Nat.pow_lt_pow_left hyx hn)
