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