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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	ltesubnnd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	ltesubnnd	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 𝑁 ) ≤ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		ltesubnnd.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		ltesubnnd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3	1	zcnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
4		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
5	2	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
6	3 4 5	addsubd	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 𝑁 ) = ( ( 𝑀 − 𝑁 ) + 1 ) )
7	1	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
8	2	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
9	7 8	ltsubrpd	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) < 𝑀 )
10	2	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11	1 10	zsubcld	⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℤ )
12		zltp1le	⊢ ( ( ( 𝑀 − 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑀 − 𝑁 ) < 𝑀 ↔ ( ( 𝑀 − 𝑁 ) + 1 ) ≤ 𝑀 ) )
13	11 1 12	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 − 𝑁 ) < 𝑀 ↔ ( ( 𝑀 − 𝑁 ) + 1 ) ≤ 𝑀 ) )
14	9 13	mpbid	⊢ ( 𝜑 → ( ( 𝑀 − 𝑁 ) + 1 ) ≤ 𝑀 )
15	6 14	eqbrtrd	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 𝑁 ) ≤ 𝑀 )