English
Let x,y be integers with x − y even and x odd. For n even, the following lifting holds: emultiplicity_2(x^n − y^n) + 1 = emultiplicity_2(x + y) + emultiplicity_2(x − y) + emultiplicity_2(n).
Русский
Пусть x,y — целые числа, причём x − y чётно и x нечётно. При чётном 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{Z},\\ \\forall n \\in \\mathbb{N},\\ (x\\ \\text{нечетно} \\land 2 \\mid x-y) \\Rightarrow \\nu_2(x^n - y^n) + 1 = \\nu_2(x+y) + \\nu_2(x-y) + \\nu_2(n)$$$
Lean4
/-- **Lifting the exponent lemma** for `p = 2` -/
theorem two_pow_sub_pow {x y : ℤ} {n : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) (hn : Even n) :
emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (2 : ℤ) n :=
by
have hy : Odd y := by
rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx
replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)
convert Even.add_odd hxy hx
abel
obtain ⟨d, hd⟩ := hn
subst hd
simp only [← two_mul, pow_mul]
have hxy4 : 4 ∣ x ^ 2 - y ^ 2 :=
by
rw [Int.dvd_iff_emod_eq_zero, Int.sub_emod, Int.sq_mod_four_eq_one_of_odd _, Int.sq_mod_four_eq_one_of_odd hy]
· simp
· simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]
rw [Int.two_pow_sub_pow' d hxy4 _, sq_sub_sq, ← Int.ofNat_mul_out, emultiplicity_mul Int.prime_two,
emultiplicity_mul Int.prime_two]
· suffices emultiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by rw [this, add_comm 1, ← add_assoc]
norm_cast
rw [FiniteMultiplicity.emultiplicity_self]
rw [Nat.finiteMultiplicity_iff]
decide
· rw [← even_iff_two_dvd, Int.not_even_iff_odd]
apply Odd.pow
simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]
