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