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 
|- ( N e. NN0 -> 0 <_ N )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 nngt0 
 |-  ( N e. NN -> 0 < N )
3 id 
 |-  ( N = 0 -> N = 0 )
4 3 eqcomd 
 |-  ( N = 0 -> 0 = N )
5 2 4 orim12i 
 |-  ( ( N e. NN \/ N = 0 ) -> ( 0 < N \/ 0 = N ) )
6 1 5 sylbi 
 |-  ( N e. NN0 -> ( 0 < N \/ 0 = N ) )
7 0re 
 |-  0 e. RR
8 nn0re 
 |-  ( N e. NN0 -> N e. RR )
9 leloe 
 |-  ( ( 0 e. RR /\ N e. RR ) -> ( 0 <_ N <-> ( 0 < N \/ 0 = N ) ) )
10 7 8 9 sylancr 
 |-  ( N e. NN0 -> ( 0 <_ N <-> ( 0 < N \/ 0 = N ) ) )
11 6 10 mpbird 
 |-  ( N e. NN0 -> 0 <_ N )