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	$$⊢\phi \to M\in \mathbb{Z}$$
	ltesubnnd.2	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	ltesubnnd	$$⊢\phi \to M+1-N\le M$$

Proof

Step	Hyp	Ref	Expression
1		ltesubnnd.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		ltesubnnd.2	$$⊢\phi \to N\in \mathbb{N}$$
3	1	zcnd	$$⊢\phi \to M\in ℂ$$
4		1cnd	$$⊢\phi \to 1\in ℂ$$
5	2	nncnd	$$⊢\phi \to N\in ℂ$$
6	3 4 5	addsubd	$$⊢\phi \to M+1-N=M-N+1$$
7	1	zred	$$⊢\phi \to M\in ℝ$$
8	2	nnrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
9	7 8	ltsubrpd	$$⊢\phi \to M-N<M$$
10	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
11	1 10	zsubcld	$$⊢\phi \to M-N\in \mathbb{Z}$$
12		zltp1le	$$⊢\left(M-N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(M-N<M\leftrightarrow M-N+1\le M\right)$$
13	11 1 12	syl2anc	$$⊢\phi \to \left(M-N<M\leftrightarrow M-N+1\le M\right)$$
14	9 13	mpbid	$$⊢\phi \to M-N+1\le M$$
15	6 14	eqbrtrd	$$⊢\phi \to M+1-N\le M$$