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