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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
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 ) − 𝑁 ) ≤ 𝑀 )