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		recn	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
3	2	negeq0d	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 = 0 ↔ - 𝑁 = 0 ) )
4	3	orbi2d	⊢ ( 𝑁 ∈ ℝ → ( ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ↔ ( - 𝑁 ∈ ℕ ∨ - 𝑁 = 0 ) ) )
5		elnn0	⊢ ( - 𝑁 ∈ ℕ0 ↔ ( - 𝑁 ∈ ℕ ∨ - 𝑁 = 0 ) )
6	4 5	syl6rbbr	⊢ ( 𝑁 ∈ ℝ → ( - 𝑁 ∈ ℕ0 ↔ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) )
7	6	orbi2d	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ↔ ( 𝑁 ∈ ℕ ∨ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) ) )
8		3orrot	⊢ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
9		3orass	⊢ ( ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ↔ ( 𝑁 ∈ ℕ ∨ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) )
10	8 9	bitri	⊢ ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( 𝑁 ∈ ℕ ∨ ( - 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) )
11	7 10	syl6rbbr	⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ↔ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )
12	11	pm5.32i	⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )
13	1 12	bitri	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ0 ) ) )