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 ) < ( 𝐶 / 𝐵 ) ) )