English
Let p be an odd prime, and x,y ∈ ℕ with p ∣ x + y and p ∤ x. If n is odd, then padicValNat p (x^n + y^n) equals padicValNat p (x + y) plus padicValNat p n.
Русский
Пусть p — нечётная простая, x,y ∈ N, p | x+y и p ∤ x; если n нечётно, то v_p(x^n + y^n) = v_p(x+y) + v_p(n).
LaTeX
$$$\\forall x,y \\in \\mathbb{N},\\ p\\text{ нечётная простая},\\ p \\mid (x+y) \\land p \\nmid x \\Rightarrow \\forall n\\in \\mathbb{N},\\ n \\text{ нечётно} \\,\\Rightarrow \\, \\mathrm{padicVal}_p(x^n + y^n) = \\mathrm{padicVal}_p(x+y) + \\mathrm{padicVal}_p(n)$$$
Lean4
theorem pow_add_pow (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : Odd n) :
padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n :=
by
rcases y with - | y
· contradiction
rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
iterate 3 rw [padicValNat_eq_emultiplicity]
· exact Nat.emultiplicity_pow_add_pow hp.out hp1 hxy hx hn
· exact (Odd.pos hn).ne'
· simp only [← Nat.pos_iff_ne_zero, add_pos_iff, Nat.succ_pos', or_true]
· exact (Nat.lt_add_left _ (pow_pos y.succ_pos _)).ne'
