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	$$⊢\mathbb{P}\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		prmssnn	$$⊢\mathbb{P}\subseteq \mathbb{N}$$
2		prmunb	$$⊢n\in \mathbb{N}\to \exists p\in \mathbb{P}n<p$$
3	2	rgen	$$⊢\forall n\in \mathbb{N}\exists p\in \mathbb{P}n<p$$
4		unben	$$⊢\left(\mathbb{P}\subseteq \mathbb{N}\wedge \forall n\in \mathbb{N}\exists p\in \mathbb{P}n<p\right)\to \mathbb{P}\approx \mathbb{N}$$
5	1 3 4	mp2an	$$⊢\mathbb{P}\approx \mathbb{N}$$