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	⊢ ℤ = { 𝑛 ∈ ℝ ∣ ( 𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ - 𝑛 ∈ ℕ ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cz	⊢ ℤ
1		vn	⊢ 𝑛
2		cr	⊢ ℝ
3	1	cv	⊢ 𝑛
4		cc0	⊢ 0
5	3 4	wceq	⊢ 𝑛 = 0
6		cn	⊢ ℕ
7	3 6	wcel	⊢ 𝑛 ∈ ℕ
8	3	cneg	⊢ - 𝑛
9	8 6	wcel	⊢ - 𝑛 ∈ ℕ
10	5 7 9	w3o	⊢ ( 𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ - 𝑛 ∈ ℕ )
11	10 1 2	crab	⊢ { 𝑛 ∈ ℝ ∣ ( 𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ - 𝑛 ∈ ℕ ) }
12	0 11	wceq	⊢ ℤ = { 𝑛 ∈ ℝ ∣ ( 𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ - 𝑛 ∈ ℕ ) }