Metamath Proof Explorer

Theorem nnm1ge0

Description: A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018)

Ref Expression
Assertion nnm1ge0 
|- ( N e. NN -> 0 <_ ( N - 1 ) )

Proof

Step Hyp Ref Expression
1 nngt0 
 |-  ( N e. NN -> 0 < N )
2 0z 
 |-  0 e. ZZ
3 nnz 
 |-  ( N e. NN -> N e. ZZ )
4 zltlem1 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 < N <-> 0 <_ ( N - 1 ) ) )
5 2 3 4 sylancr 
 |-  ( N e. NN -> ( 0 < N <-> 0 <_ ( N - 1 ) ) )
6 1 5 mpbid 
 |-  ( N e. NN -> 0 <_ ( N - 1 ) )