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

Proof

Step Hyp Ref Expression
1 0nnn ¬ 0
2 prmnn 0 0
3 1 2 mto ¬ 0