Metamath Proof Explorer

Theorem elz

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

Ref Expression
Assertion elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ x = N → x = 0 ↔ N = 0
2 eleq1 ⊢ x = N → x ∈ ℕ ↔ N ∈ ℕ
3 negeq ⊢ x = N → − x = − N
4 3 eleq1d ⊢ x = N → − x ∈ ℕ ↔ − N ∈ ℕ
5 1 2 4 3orbi123d ⊢ x = N → x = 0 ∨ x ∈ ℕ ∨ − x ∈ ℕ ↔ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
6 df-z ⊢ ℤ = x ∈ ℝ | x = 0 ∨ x ∈ ℕ ∨ − x ∈ ℕ
7 5 6 elrab2 ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ