English
m ∈ factoredNumbers(s) iff m ≠ 0 and every prime p ≤ m with p | m lies in s.
Русский
m ∈ factoredNumbers(s) тогда и только тогда, когда m ≠ 0 и каждый простейший делитель p ≤ m, делящий m, принадлежит s.
LaTeX
$$m ∈ \mathrm{factoredNumbers}(s) \iff m \neq 0 \wedge \forall p \le m, p.Prime \rightarrow p \mid m \rightarrow p \in s$$
Lean4
/-- `m` is `s`-factored if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
are in `s`. -/
theorem mem_factoredNumbers_iff_forall_le {s : Finset ℕ} {m : ℕ} :
m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, p.Prime → p ∣ m → p ∈ s :=
by
simp_rw [mem_factoredNumbers, mem_primeFactorsList']
exact
⟨fun ⟨H₀, H₁⟩ ↦ ⟨H₀, fun p _ hp₂ hp₃ ↦ H₁ p ⟨hp₂, hp₃, H₀⟩⟩, fun ⟨H₀, H₁⟩ ↦
⟨H₀, fun p ⟨hp₁, hp₂, hp₃⟩ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero hp₃) hp₂) hp₁ hp₂⟩⟩
