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