Metamath Proof Explorer

Theorem elznn

Description: Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
2 3orrot ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
3 3orass ⊢ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0 ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
4 2 3 bitri ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
5 elnn0 ⊢ − N ∈ ℕ 0 ↔ − N ∈ ℕ ∨ − N = 0
6 recn ⊢ N ∈ ℝ → N ∈ ℂ
7 6 negeq0d ⊢ N ∈ ℝ → N = 0 ↔ − N = 0
8 7 orbi2d ⊢ N ∈ ℝ → − N ∈ ℕ ∨ N = 0 ↔ − N ∈ ℕ ∨ − N = 0
9 5 8 bitr4id ⊢ N ∈ ℝ → − N ∈ ℕ 0 ↔ − N ∈ ℕ ∨ N = 0
10 9 orbi2d ⊢ N ∈ ℝ → N ∈ ℕ ∨ − N ∈ ℕ 0 ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
11 4 10 bitr4id ⊢ N ∈ ℝ → N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ ∨ − N ∈ ℕ 0
12 11 pm5.32i ⊢ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℝ ∧ N ∈ ℕ ∨ − N ∈ ℕ 0
13 1 12 bitri ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N ∈ ℕ ∨ − N ∈ ℕ 0