Theorem elz

Description: Membership in the set of integers. (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	elz	|- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( x = N -> ( x = 0 <-> N = 0 ) )
2		eleq1	|- ( x = N -> ( x e. NN <-> N e. NN ) )
3		negeq	|- ( x = N -> -u x = -u N )
4	3	eleq1d	|- ( x = N -> ( -u x e. NN <-> -u N e. NN ) )
5	1 2 4	3orbi123d	|- ( x = N -> ( ( x = 0 \/ x e. NN \/ -u x e. NN ) <-> ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
6		df-z	|- ZZ = { x e. RR | ( x = 0 \/ x e. NN \/ -u x e. NN ) }
7	5 6	elrab2	|- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )