Theorem elz

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

	Ref	Expression
Assertion	elz	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 = 0 ↔ 𝑁 = 0 ) )
2		eleq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ℕ ↔ 𝑁 ∈ ℕ ) )
3		negeq	⊢ ( 𝑥 = 𝑁 → - 𝑥 = - 𝑁 )
4	3	eleq1d	⊢ ( 𝑥 = 𝑁 → ( - 𝑥 ∈ ℕ ↔ - 𝑁 ∈ ℕ ) )
5	1 2 4	3orbi123d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ - 𝑥 ∈ ℕ ) ↔ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
6		df-z	⊢ ℤ = { 𝑥 ∈ ℝ ∣ ( 𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ - 𝑥 ∈ ℕ ) }
7	5 6	elrab2	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )