Metamath Proof Explorer

Theorem elznn

Description: Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 elz ⊢N∈ℤ↔N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ
2 3orrot ⊢N=0∨N∈ℕ∨−N∈ℕ↔N∈ℕ∨−N∈ℕ∨N=0
3 3orass ⊢N∈ℕ∨−N∈ℕ∨N=0↔N∈ℕ∨−N∈ℕ∨N=0
4 2 3 bitri ⊢N=0∨N∈ℕ∨−N∈ℕ↔N∈ℕ∨−N∈ℕ∨N=0
5 elnn0 ⊢−N∈ℕ0↔−N∈ℕ∨−N=0
6 recn ⊢N∈ℝ→N∈ℂ
7 6 negeq0d ⊢N∈ℝ→N=0↔−N=0
8 7 orbi2d ⊢N∈ℝ→−N∈ℕ∨N=0↔−N∈ℕ∨−N=0
9 5 8 bitr4id ⊢N∈ℝ→−N∈ℕ0↔−N∈ℕ∨N=0
10 9 orbi2d ⊢N∈ℝ→N∈ℕ∨−N∈ℕ0↔N∈ℕ∨−N∈ℕ∨N=0
11 4 10 bitr4id ⊢N∈ℝ→N=0∨N∈ℕ∨−N∈ℕ↔N∈ℕ∨−N∈ℕ0
12 11 pm5.32i ⊢N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ↔N∈ℝ∧N∈ℕ∨−N∈ℕ0
13 1 12 bitri ⊢N∈ℤ↔N∈ℝ∧N∈ℕ∨−N∈ℕ0