# 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}\in ℤ↔\left({N}\in {ℕ}_{0}\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$

### Proof

Step Hyp Ref Expression
1 elz ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)$
2 andi ${⊢}\left({N}\in ℝ\wedge \left(\left({N}=0\vee {N}\in ℕ\right)\vee -{N}\in ℕ\right)\right)↔\left(\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\right)\right)\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$
3 df-3or ${⊢}\left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)↔\left(\left({N}=0\vee {N}\in ℕ\right)\vee -{N}\in ℕ\right)$
4 3 anbi2i ${⊢}\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)↔\left({N}\in ℝ\wedge \left(\left({N}=0\vee {N}\in ℕ\right)\vee -{N}\in ℕ\right)\right)$
5 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
6 5 pm4.71ri ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℝ\wedge {N}\in {ℕ}_{0}\right)$
7 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
8 orcom ${⊢}\left({N}\in ℕ\vee {N}=0\right)↔\left({N}=0\vee {N}\in ℕ\right)$
9 7 8 bitri ${⊢}{N}\in {ℕ}_{0}↔\left({N}=0\vee {N}\in ℕ\right)$
10 9 anbi2i ${⊢}\left({N}\in ℝ\wedge {N}\in {ℕ}_{0}\right)↔\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\right)\right)$
11 6 10 bitri ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\right)\right)$
12 11 orbi1i ${⊢}\left({N}\in {ℕ}_{0}\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)↔\left(\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\right)\right)\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$
13 2 4 12 3bitr4i ${⊢}\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)↔\left({N}\in {ℕ}_{0}\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$
14 1 13 bitri ${⊢}{N}\in ℤ↔\left({N}\in {ℕ}_{0}\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$