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

Metamath Proof Explorer

Theorem elznn0nn

Description: Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004)

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

Proof

Step Hyp Ref Expression
1 elz ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
2 andi ⊢ ( ( 𝑁 ∈ ℝ ∧ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ∨ - 𝑁 ∈ ℕ ) ) ↔ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ) ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
3 df-3or ⊢ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ∨ - 𝑁 ∈ ℕ ) )
4 3 anbi2i ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℝ ∧ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ∨ - 𝑁 ∈ ℕ ) ) )
5 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
6 5 pm4.71ri ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) )
7 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
8 orcom ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ↔ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) )
9 7 8 bitri ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) )
10 9 anbi2i ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ) )
11 6 10 bitri ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ) )
12 11 orbi1i ⊢ ( ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) ↔ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ) ) ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
13 2 4 12 3bitr4i ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
14 1 13 bitri ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )