Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22Jun2011)
Ref  Expression  

Assertion  prmnn   ( P e. Prime > P e. NN ) 
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 ) 