Product_Plus_One_Has_New_Prime_Factor
ProvedFor any finite set S of primes, the product of all elements plus 1 has a prime factor not in S, proving the infinitude of primes.
Preamble
import Mathlib.Data.Nat.Prime.Basic import Mathlib.Tactic
Formal statement
theorem Product_Plus_One_Has_New_Prime_Factor (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : ∃ q, Nat.Prime q ∧ q ∉ S := by sorry