Definition df-z

Description: Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in Apostol p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	df-z	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cz	|- ZZ
1		vn	|- n
2		cr	|- RR
3	1	cv	|- n
4		cc0	|- 0
5	3 4	wceq	|- n = 0
6		cn	|- NN
7	3 6	wcel	|- n e. NN
8	3	cneg	|- -u n
9	8 6	wcel	|- -u n e. NN
10	5 7 9	w3o	|- ( n = 0 \/ n e. NN \/ -u n e. NN )
11	10 1 2	crab	|- { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }
12	0 11	wceq	|- ZZ = { n e. RR | ( n = 0 \/ n e. NN \/ -u n e. NN ) }