Theorem 0nnn

Description: Zero is not a positive integer. (Contributed by NM, 25-Aug-1999) Remove dependency on ax-pre-mulgt0 . (Revised by Steven Nguyen, 30-Jan-2023)

	Ref	Expression
Assertion	0nnn	$$⊢\neg 0\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		neirr	$$⊢\neg 0\ne 0$$
2		nnne0	$$⊢0\in \mathbb{N}\to 0\ne 0$$
3	1 2	mto	$$⊢\neg 0\in \mathbb{N}$$