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	syl5bb	⊢ ( 𝑁 ∈ ℝ → ( - 𝑁 ∈ ℕ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 ) ) )