Metamath Proof Explorer

Theorem ltdifltdiv

Description: If the dividend of a division is less than the difference between a real number and the divisor, the floor function of the division plus 1 is less than the division of the real number by the divisor. (Contributed by Alexander van der Vekens, 14-Apr-2018)

Ref Expression
Assertion ltdifltdiv 
|- ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( A < ( C - B ) -> ( ( |_ ` ( A / B ) ) + 1 ) < ( C / B ) ) )

Proof

Step Hyp Ref Expression
1 refldivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
2 peano2re 
 |-  ( ( |_ ` ( A / B ) ) e. RR -> ( ( |_ ` ( A / B ) ) + 1 ) e. RR )
3 1 2 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( |_ ` ( A / B ) ) + 1 ) e. RR )
4 3 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( |_ ` ( A / B ) ) + 1 ) e. RR )
5 4 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( |_ ` ( A / B ) ) + 1 ) e. RR )
6 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
7 peano2re 
 |-  ( ( A / B ) e. RR -> ( ( A / B ) + 1 ) e. RR )
8 6 7 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) + 1 ) e. RR )
9 8 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( A / B ) + 1 ) e. RR )
10 9 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( A / B ) + 1 ) e. RR )
11 rerpdivcl 
 |-  ( ( C e. RR /\ B e. RR+ ) -> ( C / B ) e. RR )
12 11 ancoms 
 |-  ( ( B e. RR+ /\ C e. RR ) -> ( C / B ) e. RR )
13 12 3adant1 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( C / B ) e. RR )
14 13 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( C / B ) e. RR )
15 1 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( |_ ` ( A / B ) ) e. RR )
16 15 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( |_ ` ( A / B ) ) e. RR )
17 6 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( A / B ) e. RR )
18 17 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( A / B ) e. RR )
19 1red 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> 1 e. RR )
20 3simpa 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( A e. RR /\ B e. RR+ ) )
21 20 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( A e. RR /\ B e. RR+ ) )
22 fldivle 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) <_ ( A / B ) )
23 21 22 syl 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( |_ ` ( A / B ) ) <_ ( A / B ) )
24 16 18 19 23 leadd1dd 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( |_ ` ( A / B ) ) + 1 ) <_ ( ( A / B ) + 1 ) )
25 rpre 
 |-  ( B e. RR+ -> B e. RR )
26 ltaddsub 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) < C <-> A < ( C - B ) ) )
27 25 26 syl3an2 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( A + B ) < C <-> A < ( C - B ) ) )
28 27 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( A + B ) < C )
29 recn 
 |-  ( ( A / B ) e. RR -> ( A / B ) e. CC )
30 6 29 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. CC )
31 30 3adant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( A / B ) e. CC )
32 rpcn 
 |-  ( B e. RR+ -> B e. CC )
33 32 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> B e. CC )
34 1cnd 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> 1 e. CC )
35 recn 
 |-  ( A e. RR -> A e. CC )
36 35 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> A e. CC )
37 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
38 37 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> B =/= 0 )
39 36 33 38 divcan1d 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( A / B ) x. B ) = A )
40 32 mulid2d 
 |-  ( B e. RR+ -> ( 1 x. B ) = B )
41 40 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( 1 x. B ) = B )
42 39 41 oveq12d 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( ( A / B ) x. B ) + ( 1 x. B ) ) = ( A + B ) )
43 31 33 34 42 joinlmuladdmuld 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( ( A / B ) + 1 ) x. B ) = ( A + B ) )
44 recn 
 |-  ( C e. RR -> C e. CC )
45 44 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> C e. CC )
46 45 33 38 divcan1d 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( C / B ) x. B ) = C )
47 43 46 breq12d 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( ( ( A / B ) + 1 ) x. B ) < ( ( C / B ) x. B ) <-> ( A + B ) < C ) )
48 47 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( ( ( A / B ) + 1 ) x. B ) < ( ( C / B ) x. B ) <-> ( A + B ) < C ) )
49 28 48 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( ( A / B ) + 1 ) x. B ) < ( ( C / B ) x. B ) )
50 17 7 syl 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( A / B ) + 1 ) e. RR )
51 simp2 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> B e. RR+ )
52 50 13 51 ltmul1d 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( ( ( A / B ) + 1 ) < ( C / B ) <-> ( ( ( A / B ) + 1 ) x. B ) < ( ( C / B ) x. B ) ) )
53 52 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( ( A / B ) + 1 ) < ( C / B ) <-> ( ( ( A / B ) + 1 ) x. B ) < ( ( C / B ) x. B ) ) )
54 49 53 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( A / B ) + 1 ) < ( C / B ) )
55 5 10 14 24 54 lelttrd 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ C e. RR ) /\ A < ( C - B ) ) -> ( ( |_ ` ( A / B ) ) + 1 ) < ( C / B ) )
56 55 ex 
 |-  ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( A < ( C - B ) -> ( ( |_ ` ( A / B ) ) + 1 ) < ( C / B ) ) )