Metamath Proof Explorer


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 ≤ 𝑁 )