Metamath Proof Explorer


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 npn<p
3 2 rgen npn<p
4 unben npn<p
5 1 3 4 mp2an