This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zltlesub

Description: If an integer N is less than or equal to a real, and we subtract a quantity less than 1 , then N is less than or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses zltlesub.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
zltlesub.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
zltlesub.nlea ⊢ ( 𝜑 → 𝑁 ≤ 𝐴 )
zltlesub.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
zltlesub.blt1 ⊢ ( 𝜑 → 𝐵 < 1 )
zltlesub.asb ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℤ )
Assertion zltlesub ( 𝜑 → 𝑁 ≤ ( 𝐴 − 𝐵 ) )

Proof

Step Hyp Ref Expression
1 zltlesub.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2 zltlesub.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 zltlesub.nlea ⊢ ( 𝜑 → 𝑁 ≤ 𝐴 )
4 zltlesub.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 zltlesub.blt1 ⊢ ( 𝜑 → 𝐵 < 1 )
6 zltlesub.asb ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℤ )
7 1 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
8 6 zred ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ )
9 8 4 readdcld ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 𝐵 ) ∈ ℝ )
10 peano2re ⊢ ( ( 𝐴 − 𝐵 ) ∈ ℝ → ( ( 𝐴 − 𝐵 ) + 1 ) ∈ ℝ )
11 8 10 syl ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 1 ) ∈ ℝ )
12 2 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13 4 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
14 12 13 npcand ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 𝐵 ) = 𝐴 )
15 3 14 breqtrrd ⊢ ( 𝜑 → 𝑁 ≤ ( ( 𝐴 − 𝐵 ) + 𝐵 ) )
16 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
17 4 16 8 5 ltadd2dd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) + 𝐵 ) < ( ( 𝐴 − 𝐵 ) + 1 ) )
18 7 9 11 15 17 lelttrd ⊢ ( 𝜑 → 𝑁 < ( ( 𝐴 − 𝐵 ) + 1 ) )
19 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐴 − 𝐵 ) ∈ ℤ ) → ( 𝑁 ≤ ( 𝐴 − 𝐵 ) ↔ 𝑁 < ( ( 𝐴 − 𝐵 ) + 1 ) ) )
20 1 6 19 syl2anc ⊢ ( 𝜑 → ( 𝑁 ≤ ( 𝐴 − 𝐵 ) ↔ 𝑁 < ( ( 𝐴 − 𝐵 ) + 1 ) ) )
21 18 20 mpbird ⊢ ( 𝜑 → 𝑁 ≤ ( 𝐴 − 𝐵 ) )