English
If p is positive and n is p-smooth, then p^e · n is (p+1)-smooth for any e.
Русский
Если p > 0 и n ∈ p-smooth, то p^e · n ∈ (p+1)-smooth для любого e.
LaTeX
$$$p \neq 0 \wedge e \in \mathbb{N} \wedge n \in \mathrm{smoothNumbers}(p) \Rightarrow p^{e} \cdot n \in \mathrm{smoothNumbers}(p+1)$$$
Lean4
/-- If `p` is positive and `n` is `p`-smooth, then every product `p^e * n` is `(p+1)`-smooth. -/
theorem pow_mul_mem_smoothNumbers {p n : ℕ} (hp : p ≠ 0) (e : ℕ) (hn : n ∈ smoothNumbers p) :
p ^ e * n ∈ smoothNumbers (succ p) := by
-- This cannot be easily reduced to `pow_mul_mem_factoredNumbers`, as there `p.Prime` is needed.
have : NoZeroDivisors ℕ := inferInstance
have hp' := pow_ne_zero e hp
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩
rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H
· rw [mem_primeFactorsList hp'] at H
exact lt_succ.mpr <| le_of_dvd hp.bot_lt <| H.1.dvd_of_dvd_pow H.2
· exact (hn.2 q H).trans <| lt_succ_self p
