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 ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ด < ( ๐ถ โˆ’ ๐ต ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) < ( ๐ถ / ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 refldivcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โˆˆ โ„ )
2 peano2re โŠข ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โˆˆ โ„ โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) โˆˆ โ„ )
3 1 2 syl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) โˆˆ โ„ )
4 3 3adant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) โˆˆ โ„ )
5 4 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) โˆˆ โ„ )
6 rerpdivcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ๐ด / ๐ต ) โˆˆ โ„ )
7 peano2re โŠข ( ( ๐ด / ๐ต ) โˆˆ โ„ โ†’ ( ( ๐ด / ๐ต ) + 1 ) โˆˆ โ„ )
8 6 7 syl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ( ๐ด / ๐ต ) + 1 ) โˆˆ โ„ )
9 8 3adant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ๐ด / ๐ต ) + 1 ) โˆˆ โ„ )
10 9 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( ๐ด / ๐ต ) + 1 ) โˆˆ โ„ )
11 rerpdivcl โŠข ( ( ๐ถ โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ๐ถ / ๐ต ) โˆˆ โ„ )
12 11 ancoms โŠข ( ( ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ถ / ๐ต ) โˆˆ โ„ )
13 12 3adant1 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ถ / ๐ต ) โˆˆ โ„ )
14 13 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ๐ถ / ๐ต ) โˆˆ โ„ )
15 1 3adant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โˆˆ โ„ )
16 15 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โˆˆ โ„ )
17 6 3adant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ด / ๐ต ) โˆˆ โ„ )
18 17 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ๐ด / ๐ต ) โˆˆ โ„ )
19 1red โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ 1 โˆˆ โ„ )
20 3simpa โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) )
21 20 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) )
22 fldivle โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โ‰ค ( ๐ด / ๐ต ) )
23 21 22 syl โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) โ‰ค ( ๐ด / ๐ต ) )
24 16 18 19 23 leadd1dd โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) โ‰ค ( ( ๐ด / ๐ต ) + 1 ) )
25 rpre โŠข ( ๐ต โˆˆ โ„+ โ†’ ๐ต โˆˆ โ„ )
26 ltaddsub โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ๐ด + ๐ต ) < ๐ถ โ†” ๐ด < ( ๐ถ โˆ’ ๐ต ) ) )
27 25 26 syl3an2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ๐ด + ๐ต ) < ๐ถ โ†” ๐ด < ( ๐ถ โˆ’ ๐ต ) ) )
28 27 biimpar โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ๐ด + ๐ต ) < ๐ถ )
29 recn โŠข ( ( ๐ด / ๐ต ) โˆˆ โ„ โ†’ ( ๐ด / ๐ต ) โˆˆ โ„‚ )
30 6 29 syl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ๐ด / ๐ต ) โˆˆ โ„‚ )
31 30 3adant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ด / ๐ต ) โˆˆ โ„‚ )
32 rpcn โŠข ( ๐ต โˆˆ โ„+ โ†’ ๐ต โˆˆ โ„‚ )
33 32 3ad2ant2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ต โˆˆ โ„‚ )
34 1cnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ 1 โˆˆ โ„‚ )
35 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
36 35 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ด โˆˆ โ„‚ )
37 rpne0 โŠข ( ๐ต โˆˆ โ„+ โ†’ ๐ต โ‰  0 )
38 37 3ad2ant2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ต โ‰  0 )
39 36 33 38 divcan1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ๐ด / ๐ต ) ยท ๐ต ) = ๐ด )
40 32 mulid2d โŠข ( ๐ต โˆˆ โ„+ โ†’ ( 1 ยท ๐ต ) = ๐ต )
41 40 3ad2ant2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( 1 ยท ๐ต ) = ๐ต )
42 39 41 oveq12d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ( ๐ด / ๐ต ) ยท ๐ต ) + ( 1 ยท ๐ต ) ) = ( ๐ด + ๐ต ) )
43 31 33 34 42 joinlmuladdmuld โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ( ๐ด / ๐ต ) + 1 ) ยท ๐ต ) = ( ๐ด + ๐ต ) )
44 recn โŠข ( ๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„‚ )
45 44 3ad2ant3 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ถ โˆˆ โ„‚ )
46 45 33 38 divcan1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ๐ถ / ๐ต ) ยท ๐ต ) = ๐ถ )
47 43 46 breq12d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ( ( ๐ด / ๐ต ) + 1 ) ยท ๐ต ) < ( ( ๐ถ / ๐ต ) ยท ๐ต ) โ†” ( ๐ด + ๐ต ) < ๐ถ ) )
48 47 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( ( ( ๐ด / ๐ต ) + 1 ) ยท ๐ต ) < ( ( ๐ถ / ๐ต ) ยท ๐ต ) โ†” ( ๐ด + ๐ต ) < ๐ถ ) )
49 28 48 mpbird โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( ( ๐ด / ๐ต ) + 1 ) ยท ๐ต ) < ( ( ๐ถ / ๐ต ) ยท ๐ต ) )
50 17 7 syl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ๐ด / ๐ต ) + 1 ) โˆˆ โ„ )
51 simp2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ๐ต โˆˆ โ„+ )
52 50 13 51 ltmul1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ( ( ๐ด / ๐ต ) + 1 ) < ( ๐ถ / ๐ต ) โ†” ( ( ( ๐ด / ๐ต ) + 1 ) ยท ๐ต ) < ( ( ๐ถ / ๐ต ) ยท ๐ต ) ) )
53 52 adantr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( ( ๐ด / ๐ต ) + 1 ) < ( ๐ถ / ๐ต ) โ†” ( ( ( ๐ด / ๐ต ) + 1 ) ยท ๐ต ) < ( ( ๐ถ / ๐ต ) ยท ๐ต ) ) )
54 49 53 mpbird โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( ๐ด / ๐ต ) + 1 ) < ( ๐ถ / ๐ต ) )
55 5 10 14 24 54 lelttrd โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โˆง ๐ด < ( ๐ถ โˆ’ ๐ต ) ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) < ( ๐ถ / ๐ต ) )
56 55 ex โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„+ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( ๐ด < ( ๐ถ โˆ’ ๐ต ) โ†’ ( ( โŒŠ โ€˜ ( ๐ด / ๐ต ) ) + 1 ) < ( ๐ถ / ๐ต ) ) )