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 
|- Prime ~~ NN

Proof

Step Hyp Ref Expression
1 prmssnn 
 |-  Prime C_ NN
2 prmunb 
 |-  ( n e. NN -> E. p e. Prime n < p )
3 2 rgen 
 |-  A. n e. NN E. p e. Prime n < p
4 unben 
 |-  ( ( Prime C_ NN /\ A. n e. NN E. p e. Prime n < p ) -> Prime ~~ NN )
5 1 3 4 mp2an 
 |-  Prime ~~ NN