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 ) )