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	|- -. 0 e. NN

Proof

Step	Hyp	Ref	Expression
1		neirr	|- -. 0 =/= 0
2		nnne0	|- ( 0 e. NN -> 0 =/= 0 )
3	1 2	mto	|- -. 0 e. NN