English
In Int, for prime p and odd p with p ∣ x − y and p ∤ x, the LTE identity holds for x^{p^a} − y^{p^a} with a ≥ 0: v_p(x^{p^a} − y^{p^a}) = v_p(x − y) + a.
Русский
В целых числах для простого p и нечетного p, если p | x−y и p ∤ x, то v_p(x^{p^a} − y^{p^a}) = v_p(x − y) + a.
LaTeX
$$For p prime and Odd p, ∀ x,y ∈ ℤ, ∀ a ∈ ℕ, emultiplicity p (x^{p^a} − y^{p^a}) = emultiplicity p (x − y) + a.$$
Lean4
theorem two_pow_two_pow_add_two_pow_two_pow {x y : ℤ} (hx : ¬2 ∣ x) (hxy : 4 ∣ x - y) (i : ℕ) :
emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑(1 : ℕ) :=
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
refine emultiplicity_eq_coe.mpr ⟨?_, ?_⟩
· rw [pow_one, ← even_iff_two_dvd]
exact hx_odd.pow.add_odd hy_odd.pow
rcases i with - | i
· grind
suffices ∀ x : ℤ, Odd x → x ^ 2 ^ (i + 1) % 4 = 1
by
rw [show (2 ^ (1 + 1) : ℤ) = 4 by simp, Int.dvd_iff_emod_eq_zero, Int.add_emod, this _ hx_odd, this _ hy_odd]
decide
intro x hx
rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]
