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

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 ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )

Proof

Step Hyp Ref Expression
1 elz ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
2 3orrot ⊢ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
3 3orass ⊢ ( ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ↔ ( 𝑁 ∈ ℕ ∨ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) )
4 2 3 bitri ⊢ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( 𝑁 ∈ ℕ ∨ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) )
5 elnn0 ⊢ ( - 𝑁 ∈ ℕ0 ↔ ( - 𝑁 ∈ ℕ ∨ - 𝑁 = 0 ) )
6 recn ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
7 6 negeq0d ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 = 0 ↔ - 𝑁 = 0 ) )
8 7 orbi2d ⊢ ( 𝑁 ∈ ℝ → ( ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ↔ ( - 𝑁 ∈ ℕ ∨ - 𝑁 = 0 ) ) )
9 5 8 bitr4id ⊢ ( 𝑁 ∈ ℝ → ( - 𝑁 ∈ ℕ0 ↔ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) )
10 9 orbi2d ⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ↔ ( 𝑁 ∈ ℕ ∨ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) ) )
11 4 10 bitr4id ⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )
12 11 pm5.32i ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )
13 1 12 bitri ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )