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 ( 𝜑𝑁 ≤ ( 𝐴𝐵 ) )