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 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		0nnn	⊢ ¬ 0 ∈ ℕ
2		prmnn	⊢ ( 0 ∈ ℙ → 0 ∈ ℕ )
3	1 2	mto	⊢ ¬ 0 ∈ ℙ