English
Let x,y be natural numbers with x ≡ y (mod 2) and x − y ≡ 0 (mod 2). For even n, the 2-adic valuation formula holds: ν_2(x^n − y^n) + 1 = ν_2(x+y) + ν_2(x−y) + ν_2(n).
Русский
Пусть x,y — натуральные числа с парами по 2. Для чётного n выполняется: v_2(x^n − y^n) + 1 = v_2(x+y) + v_2(x−y) + v_2(n).
LaTeX
$$$\\forall x,y \\in \\mathbb{N},\\ \\forall n \\in \\mathbb{N},\\ (2 \\mid x - y) \\Rightarrow \\nu_2(x^n - y^n) + 1 = \\nu_2(x+y) + \\nu_2(x-y) + \\nu_2(n)$$$
Lean4
theorem two_pow_sub_pow {x y : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) {n : ℕ} (hn : Even n) :
emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n :=
by
obtain hyx | hyx := le_total y x
· iterate 3 rw [← Int.natCast_emultiplicity]
simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add, Int.natCast_pow]
rw [← Int.natCast_dvd_natCast] at hx
rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy
convert Int.two_pow_sub_pow hxy hx hn using 2
rw [← Int.natCast_emultiplicity]
rfl
·
simp only [Nat.sub_eq_zero_iff_le.mpr hyx, Nat.sub_eq_zero_iff_le.mpr (pow_le_pow_left' hyx n), emultiplicity_zero,
top_add, add_top]
