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 )