Theorem 0z

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002)

	Ref	Expression
Assertion	0z	|- 0 e. ZZ

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		eqid	|- 0 = 0
3	2	3mix1i	|- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz	|- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1 3 4	mpbir2an	|- 0 e. ZZ