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 
|- ( ph -> N e. ZZ )
zltlesub.a 
|- ( ph -> A e. RR )
zltlesub.nlea 
|- ( ph -> N <_ A )
zltlesub.b 
|- ( ph -> B e. RR )
zltlesub.blt1 
|- ( ph -> B < 1 )
zltlesub.asb 
|- ( ph -> ( A - B ) e. ZZ )
Assertion zltlesub 
|- ( ph -> N <_ ( A - B ) )

Proof

Step Hyp Ref Expression
1 zltlesub.n 
 |-  ( ph -> N e. ZZ )
2 zltlesub.a 
 |-  ( ph -> A e. RR )
3 zltlesub.nlea 
 |-  ( ph -> N <_ A )
4 zltlesub.b 
 |-  ( ph -> B e. RR )
5 zltlesub.blt1 
 |-  ( ph -> B < 1 )
6 zltlesub.asb 
 |-  ( ph -> ( A - B ) e. ZZ )
7 1 zred 
 |-  ( ph -> N e. RR )
8 6 zred 
 |-  ( ph -> ( A - B ) e. RR )
9 8 4 readdcld 
 |-  ( ph -> ( ( A - B ) + B ) e. RR )
10 peano2re 
 |-  ( ( A - B ) e. RR -> ( ( A - B ) + 1 ) e. RR )
11 8 10 syl 
 |-  ( ph -> ( ( A - B ) + 1 ) e. RR )
12 2 recnd 
 |-  ( ph -> A e. CC )
13 4 recnd 
 |-  ( ph -> B e. CC )
14 12 13 npcand 
 |-  ( ph -> ( ( A - B ) + B ) = A )
15 3 14 breqtrrd 
 |-  ( ph -> N <_ ( ( A - B ) + B ) )
16 1red 
 |-  ( ph -> 1 e. RR )
17 4 16 8 5 ltadd2dd 
 |-  ( ph -> ( ( A - B ) + B ) < ( ( A - B ) + 1 ) )
18 7 9 11 15 17 lelttrd 
 |-  ( ph -> N < ( ( A - B ) + 1 ) )
19 zleltp1 
 |-  ( ( N e. ZZ /\ ( A - B ) e. ZZ ) -> ( N <_ ( A - B ) <-> N < ( ( A - B ) + 1 ) ) )
20 1 6 19 syl2anc 
 |-  ( ph -> ( N <_ ( A - B ) <-> N < ( ( A - B ) + 1 ) ) )
21 18 20 mpbird 
 |-  ( ph -> N <_ ( A - B ) )