Metamath Proof Explorer

Theorem prmnn

Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion prmnn 
|- ( P e. Prime -> P e. NN )

Proof

Step Hyp Ref Expression
1 isprm 
 |-  ( P e. Prime <-> ( P e. NN /\ { z e. NN | z || P } ~~ 2o ) )
2 1 simplbi 
 |-  ( P e. Prime -> P e. NN )