English
If p is prime and n ∈ factoredNumbers(s), then p^e · n ∈ factoredNumbers(insert p s).
Русский
Если p простое и n ∈ factoredNumbers(s), то p^e · n ∈ factoredNumbers(s ∪ {p}).
LaTeX
$$p ^ e * n ∈ factoredNumbers (insert p s)$$
Lean4
/-- If `p` is a prime and `n` is `s`-factored, then every product `p^e * n`
is `s ∪ {p}`-factored. -/
theorem pow_mul_mem_factoredNumbers {s : Finset ℕ} {p n : ℕ} (hp : p.Prime) (e : ℕ) (hn : n ∈ factoredNumbers s) :
p ^ e * n ∈ factoredNumbers (insert p s) :=
by
have hp' := pow_ne_zero e hp.ne_zero
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
rw [(prime_dvd_prime_iff_eq H.1 hp).mp <| H.1.dvd_of_dvd_pow H.2]
exact Finset.mem_insert_self p s
· exact Finset.mem_insert_of_mem <| hn.2 _ H
