English
Let p be prime. If p^{n+1} ∣ a^{n+1} b^{n} and p^2 ∤ b, then p ∣ a.
Русский
Пусть p простое. Если p^{n+1} делит a^{n+1} b^{n} и p^2 не делит b, то p делит a.
LaTeX
$$$\\text{Prime}(p) \\Rightarrow (p^{n+1} \\mid a^{n+1} b^{n}) \\land (p^2 \\nmid b) \\Rightarrow p \\mid a.$$$
Lean4
theorem dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd [CancelCommMonoidWithZero M] {p a b : M} {n : ℕ} (hp : Prime p)
(hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 ∣ b) : p ∣ a := by
-- Suppose `p ∣ b`, write `b = p * x` and `hy : a ^ n.succ * b ^ n = p ^ n.succ * y`.
rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv
· exact hp.dvd_of_dvd_pow H
obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv
obtain ⟨y, hy⟩ := hpow
have : a ^ n.succ * x ^ n = p * y :=
by
refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n), mul_assoc]
-- So `p ∣ a` (and we're done) or `p ∣ x`, which can't be the case since it implies `p^2 ∣ b`.
refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)
obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx
rw [pow_two, ← mul_assoc]
exact dvd_mul_right _ _
