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 ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )

Proof

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