English
Let x,y be integers with x − y ≡ 0 mod 4 and x odd. For any natural n, the 2-adic valuation of x^n − y^n equals the sum of the 2-adic valuations of x − y and n: ν_2(x^n − y^n) = ν_2(x − y) + ν_2(n).
Русский
Пусть x,y — целые числа, где x − y кратно 4 и x нечетно. Тогда для любого n: v_2(x^n − y^n) = v_2(x − y) + v_2(n).
LaTeX
$$$\\forall x,y \\in \\mathbb{Z},\\ \\forall n \\in \\mathbb{N},\\ (4 \\mid x - y \\land x \\text{ нечетно}) \\Rightarrow \\nu_2\\bigl(x^n - y^n\\bigr) = \\nu_2(x - y) + \\nu_2(n)$$$
Lean4
theorem two_pow_sub_pow' {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 ∣ x) :
emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (2 : ℤ) n :=
by
have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)
have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
rcases n with - | n
· simp only [pow_zero, sub_self, emultiplicity_zero, Int.ofNat_zero, add_top]
have h : FiniteMultiplicity 2 n.succ := Nat.finiteMultiplicity_iff.mpr ⟨by simp, n.succ_pos⟩
simp only [Nat.succ_eq_add_one] at h
rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩
rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime, Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
· norm_cast
rw [h.emultiplicity_eq_multiplicity]
· exact Int.prime_two
· simpa only [even_iff_two_dvd] using hx_odd.pow.sub_odd hy_odd.pow
· simpa only [even_iff_two_dvd, ← Int.not_even_iff_odd] using hx_odd.pow
norm_cast
contrapose! hpn
rw [pow_succ]
conv_rhs => rw [hk]
exact mul_dvd_mul_left _ hpn
