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∈ℕ