English
If s contains all primes below N, then nonzero non-s-factored numbers are at least N.
Русский
Если s содержит все простые числа ниже N, то ненулевые числа вне s-факторизации не меньше N.
LaTeX
$$(factoredNumbers(s))^c \ {0} ⊆ {n | N ≤ n}$$
Lean4
/-- The non-zero non-`s`-factored numbers are `≥ N` when `s` contains all primes less than `N`. -/
theorem factoredNumbers_compl {N : ℕ} {s : Finset ℕ} (h : primesBelow N ≤ s) :
(factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n} := by
intro n hn
simp only [Set.mem_compl_iff, mem_factoredNumbers, Set.mem_diff, ne_eq, not_and, not_forall, exists_prop,
Set.mem_singleton_iff] at hn
simp only [Set.mem_setOf_eq]
obtain ⟨p, hp₁, hp₂⟩ := hn.1 hn.2
have : N ≤ p := by
contrapose! hp₂
exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩
exact this.trans <| le_of_mem_primeFactorsList hp₁
