Theorem prminf

Description: There are an infinite number of primes. Theorem 1.7 in ApostolNT p. 16. (Contributed by Paul Chapman, 28-Nov-2012)

	Ref	Expression
Assertion	prminf	⊢ ℙ ≈ ℕ

Proof

Step	Hyp	Ref	Expression
1		prmssnn	⊢ ℙ ⊆ ℕ
2		prmunb	⊢ ( 𝑛 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 )
3	2	rgen	⊢ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝
4		unben	⊢ ( ( ℙ ⊆ ℕ ∧ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 ) → ℙ ≈ ℕ )
5	1 3 4	mp2an	⊢ ℙ ≈ ℕ