Theorem 0nprm

Description: 0 is not a prime number. Already the 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	$$⊢\neg 0\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		0nnn	$$⊢\neg 0\in \mathbb{N}$$
2		prmnn	$$⊢0\in \mathbb{P}\to 0\in \mathbb{N}$$
3	1 2	mto	$$⊢\neg 0\in \mathbb{P}$$