This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
6 3 4 5 addsubd 
 |-  ( 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 )