This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elznn0

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

Ref Expression
Assertion elznn0 ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )

Proof

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