This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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