Theorem infpn

Description: There exist infinitely many prime numbers: for any positive integer N , there exists a prime number j greater than N . (See infpn2 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006)

	Ref	Expression
Assertion	infpn	$$⊢N\in \mathbb{N}\to \exists j\in \mathbb{N}\left(N<j\wedge \forall k\in \mathbb{N}\left(\frac{j}{k}\in \mathbb{N}\to \left(k=1\vee k=j\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢N!+1=N!+1$$
2	1	infpnlem2	$$⊢N\in \mathbb{N}\to \exists j\in \mathbb{N}\left(N<j\wedge \forall k\in \mathbb{N}\left(\frac{j}{k}\in \mathbb{N}\to \left(k=1\vee k=j\right)\right)\right)$$