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