This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∨ 𝑛 ∈ ℕ ∨ - 𝑛 ∈ ℕ ) }