# Metamath Proof Explorer

## Theorem ltesubnnd

Description: Subtracting an integer number from another number decreases it. See ltsubrpd . (Contributed by Thierry Arnoux, 18-Apr-2017)

Ref Expression
Hypotheses ltesubnnd.1
`|- ( ph -> M e. ZZ )`
ltesubnnd.2
`|- ( ph -> N e. NN )`
Assertion ltesubnnd
`|- ( ph -> ( ( M + 1 ) - N ) <_ M )`

### Proof

Step Hyp Ref Expression
1 ltesubnnd.1
` |-  ( ph -> M e. ZZ )`
2 ltesubnnd.2
` |-  ( ph -> N e. NN )`
3 1 zcnd
` |-  ( ph -> M e. CC )`
4 1cnd
` |-  ( ph -> 1 e. CC )`
5 2 nncnd
` |-  ( ph -> N e. CC )`
` |-  ( ph -> ( ( M + 1 ) - N ) = ( ( M - N ) + 1 ) )`
7 1 zred
` |-  ( ph -> M e. RR )`
8 2 nnrpd
` |-  ( ph -> N e. RR+ )`
9 7 8 ltsubrpd
` |-  ( ph -> ( M - N ) < M )`
10 2 nnzd
` |-  ( ph -> N e. ZZ )`
11 1 10 zsubcld
` |-  ( ph -> ( M - N ) e. ZZ )`
12 zltp1le
` |-  ( ( ( M - N ) e. ZZ /\ M e. ZZ ) -> ( ( M - N ) < M <-> ( ( M - N ) + 1 ) <_ M ) )`
13 11 1 12 syl2anc
` |-  ( ph -> ( ( M - N ) < M <-> ( ( M - N ) + 1 ) <_ M ) )`
14 9 13 mpbid
` |-  ( ph -> ( ( M - N ) + 1 ) <_ M )`
15 6 14 eqbrtrd
` |-  ( ph -> ( ( M + 1 ) - N ) <_ M )`