Metamath Proof Explorer

Theorem elznn0nn

Description: Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004)

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

Proof

Step Hyp Ref Expression
1 elz ⊢N∈ℤ↔N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ
2 andi ⊢N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ↔N∈ℝ∧N=0∨N∈ℕ∨N∈ℝ∧−N∈ℕ
3 df-3or ⊢N=0∨N∈ℕ∨−N∈ℕ↔N=0∨N∈ℕ∨−N∈ℕ
4 3 anbi2i ⊢N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ↔N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ
5 nn0re ⊢N∈ℕ0→N∈ℝ
6 5 pm4.71ri ⊢N∈ℕ0↔N∈ℝ∧N∈ℕ0
7 elnn0 ⊢N∈ℕ0↔N∈ℕ∨N=0
8 orcom ⊢N∈ℕ∨N=0↔N=0∨N∈ℕ
9 7 8 bitri ⊢N∈ℕ0↔N=0∨N∈ℕ
10 9 anbi2i ⊢N∈ℝ∧N∈ℕ0↔N∈ℝ∧N=0∨N∈ℕ
11 6 10 bitri ⊢N∈ℕ0↔N∈ℝ∧N=0∨N∈ℕ
12 11 orbi1i ⊢N∈ℕ0∨N∈ℝ∧−N∈ℕ↔N∈ℝ∧N=0∨N∈ℕ∨N∈ℝ∧−N∈ℕ
13 2 4 12 3bitr4i ⊢N∈ℝ∧N=0∨N∈ℕ∨−N∈ℕ↔N∈ℕ0∨N∈ℝ∧−N∈ℕ
14 1 13 bitri ⊢N∈ℤ↔N∈ℕ0∨N∈ℝ∧−N∈ℕ