This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0nprm

Description: 0 is not a prime number. Already Definition df-prm excludes 0 from being prime ( Prime = { p e. NN | ... ), but even if p e. NN0 was allowed, the condition { n e. NN | n || p } ~2o would not hold for p = 0 , because { n e. NN | n || 0 } = NN , see dvds0 , and -. NN ~2o (there are more than 2 positive integers). (Contributed by AV, 29-May-2023)

Ref Expression
Assertion 0nprm 
|- -. 0 e. Prime

Proof

Step Hyp Ref Expression
1 0nnn 
 |-  -. 0 e. NN
2 prmnn 
 |-  ( 0 e. Prime -> 0 e. NN )
3 1 2 mto 
 |-  -. 0 e. Prime