Theorem nn0ge0

Description: A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004) (Revised by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
3		id	⊢ ( 𝑁 = 0 → 𝑁 = 0 )
4	3	eqcomd	⊢ ( 𝑁 = 0 → 0 = 𝑁 )
5	2 4	orim12i	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 0 < 𝑁 ∨ 0 = 𝑁 ) )
6	1 5	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( 0 < 𝑁 ∨ 0 = 𝑁 ) )
7		0re	⊢ 0 ∈ ℝ
8		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
9		leloe	⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑁 ↔ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
10	7 8 9	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ≤ 𝑁 ↔ ( 0 < 𝑁 ∨ 0 = 𝑁 ) ) )
11	6 10	mpbird	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )