# Metamath Proof Explorer

## Theorem elnn0z

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

Ref Expression
Assertion elnn0z $⊢ N ∈ ℕ 0 ↔ N ∈ ℤ ∧ 0 ≤ N$

### Proof

Step Hyp Ref Expression
1 elnn0 $⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0$
2 elnnz $⊢ N ∈ ℕ ↔ N ∈ ℤ ∧ 0 < N$
3 eqcom $⊢ N = 0 ↔ 0 = N$
4 2 3 orbi12i $⊢ N ∈ ℕ ∨ N = 0 ↔ N ∈ ℤ ∧ 0 < N ∨ 0 = N$
5 id $⊢ N ∈ ℤ → N ∈ ℤ$
6 0z $⊢ 0 ∈ ℤ$
7 eleq1 $⊢ 0 = N → 0 ∈ ℤ ↔ N ∈ ℤ$
8 6 7 mpbii $⊢ 0 = N → N ∈ ℤ$
9 5 8 jaoi $⊢ N ∈ ℤ ∨ 0 = N → N ∈ ℤ$
10 orc $⊢ N ∈ ℤ → N ∈ ℤ ∨ 0 = N$
11 9 10 impbii $⊢ N ∈ ℤ ∨ 0 = N ↔ N ∈ ℤ$
12 11 anbi1i $⊢ N ∈ ℤ ∨ 0 = N ∧ 0 < N ∨ 0 = N ↔ N ∈ ℤ ∧ 0 < N ∨ 0 = N$
13 ordir $⊢ N ∈ ℤ ∧ 0 < N ∨ 0 = N ↔ N ∈ ℤ ∨ 0 = N ∧ 0 < N ∨ 0 = N$
14 0re $⊢ 0 ∈ ℝ$
15 zre $⊢ N ∈ ℤ → N ∈ ℝ$
16 leloe $⊢ 0 ∈ ℝ ∧ N ∈ ℝ → 0 ≤ N ↔ 0 < N ∨ 0 = N$
17 14 15 16 sylancr $⊢ N ∈ ℤ → 0 ≤ N ↔ 0 < N ∨ 0 = N$
18 17 pm5.32i $⊢ N ∈ ℤ ∧ 0 ≤ N ↔ N ∈ ℤ ∧ 0 < N ∨ 0 = N$
19 12 13 18 3bitr4i $⊢ N ∈ ℤ ∧ 0 < N ∨ 0 = N ↔ N ∈ ℤ ∧ 0 ≤ N$
20 1 4 19 3bitri $⊢ N ∈ ℕ 0 ↔ N ∈ ℤ ∧ 0 ≤ N$