Theorem elnn0z

Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004)

	Ref	Expression
Assertion	elnn0z	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		elnnz	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
3		eqcom	⊢ ( 𝑁 = 0 ↔ 0 = 𝑁 )
4	2 3	orbi12i	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) ∨ 0 = 𝑁 ) )
5		id	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
6		0z	⊢ 0 ∈ ℤ
7		eleq1	⊢ ( 0 = 𝑁 → ( 0 ∈ ℤ ↔ 𝑁 ∈ ℤ ) )
8	6 7	mpbii	⊢ ( 0 = 𝑁 → 𝑁 ∈ ℤ )
9	5 8	jaoi	⊢ ( ( 𝑁 ∈ ℤ ∨ 0 = 𝑁 ) → 𝑁 ∈ ℤ )
10		orc	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ℤ ∨ 0 = 𝑁 ) )
11	9 10	impbii	⊢ ( ( 𝑁 ∈ ℤ ∨ 0 = 𝑁 ) ↔ 𝑁 ∈ ℤ )
12	11	anbi1i	⊢ ( ( ( 𝑁 ∈ ℤ ∨ 0 = 𝑁 ) ∧ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
13		ordir	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) ∨ 0 = 𝑁 ) ↔ ( ( 𝑁 ∈ ℤ ∨ 0 = 𝑁 ) ∧ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
14		0re	⊢ 0 ∈ ℝ
15		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
16		leloe	⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑁 ↔ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
17	14 15 16	sylancr	⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑁 ↔ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
18	17	pm5.32i	⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
19	12 13 18	3bitr4i	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) ∨ 0 = 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
20	1 4 19	3bitri	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )