Metamath Proof Explorer

Theorem nn0p1gt0

Description: A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018)

Ref Expression
Assertion nn0p1gt0 
|- ( N e. NN0 -> 0 < ( N + 1 ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 1red 
 |-  ( N e. NN0 -> 1 e. RR )
3 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
4 0lt1 
 |-  0 < 1
5 4 a1i 
 |-  ( N e. NN0 -> 0 < 1 )
6 1 2 3 5 addgegt0d 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )