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

### Proof

Step Hyp Ref Expression
1 ltesubnnd.1 ${⊢}{\phi }\to {M}\in ℤ$
2 ltesubnnd.2 ${⊢}{\phi }\to {N}\in ℕ$
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 ℤ$
11 1 10 zsubcld ${⊢}{\phi }\to {M}-{N}\in ℤ$
12 zltp1le ${⊢}\left({M}-{N}\in ℤ\wedge {M}\in ℤ\right)\to \left({M}-{N}<{M}↔{M}-{N}+1\le {M}\right)$
13 11 1 12 syl2anc ${⊢}{\phi }\to \left({M}-{N}<{M}↔{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}$