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 recn ⊢ N ∈ ℝ → N ∈ ℂ
3 2 negeq0d ⊢ N ∈ ℝ → N = 0 ↔ − N = 0
4 3 orbi2d ⊢ N ∈ ℝ → − N ∈ ℕ ∨ N = 0 ↔ − N ∈ ℕ ∨ − N = 0
5 elnn0 ⊢ − N ∈ ℕ 0 ↔ − N ∈ ℕ ∨ − N = 0
6 4 5 syl6rbbr ⊢ N ∈ ℝ → − N ∈ ℕ 0 ↔ − N ∈ ℕ ∨ N = 0
7 6 orbi2d ⊢ N ∈ ℝ → N ∈ ℕ ∨ − N ∈ ℕ 0 ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
8 3orrot ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
9 3orass ⊢ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0 ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
10 8 9 bitri ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
11 7 10 syl6rbbr ⊢ 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