Metamath Proof Explorer

Theorem elznn0nn

Description: Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004)

Ref Expression
Assertion elznn0nn ⊢ N ∈ ℤ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ

Proof

Step Hyp Ref Expression
1 elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
2 andi ⊢ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ N ∈ ℝ ∧ − N ∈ ℕ
3 df-3or ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
4 3 anbi2i ⊢ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
5 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
6 5 pm4.71ri ⊢ N ∈ ℕ 0 ↔ N ∈ ℝ ∧ N ∈ ℕ 0
7 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
8 orcom ⊢ N ∈ ℕ ∨ N = 0 ↔ N = 0 ∨ N ∈ ℕ
9 7 8 bitri ⊢ N ∈ ℕ 0 ↔ N = 0 ∨ N ∈ ℕ
10 9 anbi2i ⊢ N ∈ ℝ ∧ N ∈ ℕ 0 ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ
11 6 10 bitri ⊢ N ∈ ℕ 0 ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ
12 11 orbi1i ⊢ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ N ∈ ℝ ∧ − N ∈ ℕ
13 2 4 12 3bitr4i ⊢ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ
14 1 13 bitri ⊢ N ∈ ℤ ↔ N ∈ ℕ 0 ∨ N ∈ ℝ ∧ − N ∈ ℕ