Metamath Proof Explorer

Theorem nn0ge0i

Description: Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Hypothesis nn0ge0i.1 
|- N e. NN0
Assertion nn0ge0i 
|- 0 <_ N

Proof

Step Hyp Ref Expression
1 nn0ge0i.1 
 |-  N e. NN0
2 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
3 1 2 ax-mp 
 |-  0 <_ N