English
Let x,y be integers with x − y divisible by 4 and x odd. Then for every natural number n, the 2-adic valuation of x^{2^n} − y^{2^n} equals the 2-adic valuation of x − y, plus n.
Русский
Пусть x, y — целые числа, причём x − y делится на 4 и x нечетно. Тогда для каждого натурального числа n выполняется: v_2(x^{2^n} − y^{2^n}) = v_2(x − y) + 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^{2^n}-y^{2^n}\\bigr) = \\nu_2(x-y) + n$$$
Lean4
theorem two_pow_two_pow_sub_pow_two_pow {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 ∣ x) :
emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + n := by
simp only [pow_two_pow_sub_pow_two_pow n, emultiplicity_mul Int.prime_two, Finset.emultiplicity_prod Int.prime_two,
add_comm, Nat.cast_one, Finset.sum_const, Finset.card_range, nsmul_one,
Int.two_pow_two_pow_add_two_pow_two_pow hx hxy]
