Metamath Proof Explorer

Theorem elznn0

Description: Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004)

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

Proof

Step Hyp Ref Expression
1 elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
2 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
3 2 a1i ⊢ N ∈ ℝ → N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
4 elnn0 ⊢ − N ∈ ℕ 0 ↔ − N ∈ ℕ ∨ − N = 0
5 recn ⊢ N ∈ ℝ → N ∈ ℂ
6 0cn ⊢ 0 ∈ ℂ
7 negcon1 ⊢ N ∈ ℂ ∧ 0 ∈ ℂ → − N = 0 ↔ − 0 = N
8 5 6 7 sylancl ⊢ N ∈ ℝ → − N = 0 ↔ − 0 = N
9 neg0 ⊢ − 0 = 0
10 9 eqeq1i ⊢ − 0 = N ↔ 0 = N
11 eqcom ⊢ 0 = N ↔ N = 0
12 10 11 bitri ⊢ − 0 = N ↔ N = 0
13 8 12 bitrdi ⊢ N ∈ ℝ → − N = 0 ↔ N = 0
14 13 orbi2d ⊢ N ∈ ℝ → − N ∈ ℕ ∨ − N = 0 ↔ − N ∈ ℕ ∨ N = 0
15 4 14 bitrid ⊢ N ∈ ℝ → − N ∈ ℕ 0 ↔ − N ∈ ℕ ∨ N = 0
16 3 15 orbi12d ⊢ N ∈ ℝ → N ∈ ℕ 0 ∨ − N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0 ∨ − N ∈ ℕ ∨ N = 0
17 3orass ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
18 orcom ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0
19 orordir ⊢ N ∈ ℕ ∨ − N ∈ ℕ ∨ N = 0 ↔ N ∈ ℕ ∨ N = 0 ∨ − N ∈ ℕ ∨ N = 0
20 17 18 19 3bitrri ⊢ N ∈ ℕ ∨ N = 0 ∨ − N ∈ ℕ ∨ N = 0 ↔ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
21 16 20 bitr2di ⊢ N ∈ ℝ → N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℕ 0 ∨ − N ∈ ℕ 0
22 21 pm5.32i ⊢ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ ↔ N ∈ ℝ ∧ N ∈ ℕ 0 ∨ − N ∈ ℕ 0
23 1 22 bitri ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N ∈ ℕ 0 ∨ − N ∈ ℕ 0