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 ⊢ φ → M ∈ ℤ
ltesubnnd.2 ⊢ φ → N ∈ ℕ
Assertion ltesubnnd ⊢ φ → M + 1 - N ≤ M

Proof

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