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 ⊢ φ → N ∈ ℤ
zltlesub.a ⊢ φ → A ∈ ℝ
zltlesub.nlea ⊢ φ → N ≤ A
zltlesub.b ⊢ φ → B ∈ ℝ
zltlesub.blt1 ⊢ φ → B < 1
zltlesub.asb ⊢ φ → A − B ∈ ℤ
Assertion zltlesub ⊢ φ → N ≤ A − B

Proof

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