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	$$⊢\mathbb{Z}=\left\{n\in ℝ|\left(n=0\vee n\in \mathbb{N}\vee -n\in \mathbb{N}\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cz	$$class\mathbb{Z}$$
1		vn	$$setvarn$$
2		cr	$$classℝ$$
3	1	cv	$$setvarn$$
4		cc0	$$class0$$
5	3 4	wceq	$$wffn=0$$
6		cn	$$class\mathbb{N}$$
7	3 6	wcel	$$wffn\in \mathbb{N}$$
8	3	cneg	$$class\left(-n\right)$$
9	8 6	wcel	$$wff-n\in \mathbb{N}$$
10	5 7 9	w3o	$$wff\left(n=0\vee n\in \mathbb{N}\vee -n\in \mathbb{N}\right)$$
11	10 1 2	crab	$$class\left\{n\in ℝ|\left(n=0\vee n\in \mathbb{N}\vee -n\in \mathbb{N}\right)\right\}$$
12	0 11	wceq	$$wff\mathbb{Z}=\left\{n\in ℝ|\left(n=0\vee n\in \mathbb{N}\vee -n\in \mathbb{N}\right)\right\}$$