# Metamath Proof Explorer

## Theorem elznn0

Description: Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion elznn0 ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\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 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
3 2 a1i ${⊢}{N}\in ℝ\to \left({N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)\right)$
4 elnn0 ${⊢}-{N}\in {ℕ}_{0}↔\left(-{N}\in ℕ\vee -{N}=0\right)$
5 recn ${⊢}{N}\in ℝ\to {N}\in ℂ$
6 0cn ${⊢}0\in ℂ$
7 negcon1 ${⊢}\left({N}\in ℂ\wedge 0\in ℂ\right)\to \left(-{N}=0↔-0={N}\right)$
8 5 6 7 sylancl ${⊢}{N}\in ℝ\to \left(-{N}=0↔-0={N}\right)$
9 neg0 ${⊢}-0=0$
10 9 eqeq1i ${⊢}-0={N}↔0={N}$
11 eqcom ${⊢}0={N}↔{N}=0$
12 10 11 bitri ${⊢}-0={N}↔{N}=0$
13 8 12 syl6bb ${⊢}{N}\in ℝ\to \left(-{N}=0↔{N}=0\right)$
14 13 orbi2d ${⊢}{N}\in ℝ\to \left(\left(-{N}\in ℕ\vee -{N}=0\right)↔\left(-{N}\in ℕ\vee {N}=0\right)\right)$
15 4 14 syl5bb ${⊢}{N}\in ℝ\to \left(-{N}\in {ℕ}_{0}↔\left(-{N}\in ℕ\vee {N}=0\right)\right)$
16 3 15 orbi12d ${⊢}{N}\in ℝ\to \left(\left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)↔\left(\left({N}\in ℕ\vee {N}=0\right)\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)$
17 3orass ${⊢}\left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)↔\left({N}=0\vee \left({N}\in ℕ\vee -{N}\in ℕ\right)\right)$
18 orcom ${⊢}\left({N}=0\vee \left({N}\in ℕ\vee -{N}\in ℕ\right)\right)↔\left(\left({N}\in ℕ\vee -{N}\in ℕ\right)\vee {N}=0\right)$
19 orordir ${⊢}\left(\left({N}\in ℕ\vee -{N}\in ℕ\right)\vee {N}=0\right)↔\left(\left({N}\in ℕ\vee {N}=0\right)\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)$
20 17 18 19 3bitrri ${⊢}\left(\left({N}\in ℕ\vee {N}=0\right)\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)↔\left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)$
21 16 20 syl6rbb ${⊢}{N}\in ℝ\to \left(\left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)↔\left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)$
22 21 pm5.32i ${⊢}\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)↔\left({N}\in ℝ\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)$
23 1 22 bitri ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)$