| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvfsumlem4.2 | . . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑆) | 
| 2 |  | fzfid 14014 | . . . . . . 7
⊢ (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin) | 
| 3 |  | dvfsum.b2 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) | 
| 4 | 3 | ralrimiva 3146 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ) | 
| 5 |  | elfzuz 13560 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ≥‘𝑀)) | 
| 6 |  | dvfsum.z | . . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 7 | 5, 6 | eleqtrrdi 2852 | . . . . . . . 8
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ 𝑍) | 
| 8 |  | dvfsum.c | . . . . . . . . . 10
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) | 
| 9 | 8 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) | 
| 10 | 9 | rspccva 3621 | . . . . . . . 8
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ) | 
| 11 | 4, 7, 10 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ) | 
| 12 | 2, 11 | fsumrecl 15770 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ) | 
| 13 |  | dvfsum.a | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) | 
| 14 | 13 | ralrimiva 3146 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ) | 
| 15 |  | nfcsb1v 3923 | . . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 | 
| 16 | 15 | nfel1 2922 | . . . . . . . 8
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ | 
| 17 |  | csbeq1a 3913 | . . . . . . . . 9
⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴) | 
| 18 | 17 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 19 | 16, 18 | rspc 3610 | . . . . . . 7
⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 20 | 1, 14, 19 | sylc 65 | . . . . . 6
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ) | 
| 21 | 12, 20 | resubcld 11691 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) | 
| 22 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑥𝑌 | 
| 23 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 | 
| 24 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑥
− | 
| 25 | 23, 24, 15 | nfov 7461 | . . . . . 6
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) | 
| 26 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌)) | 
| 27 | 26 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌))) | 
| 28 | 27 | sumeq1d 15736 | . . . . . . 7
⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶) | 
| 29 | 28, 17 | oveq12d 7449 | . . . . . 6
⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 30 |  | dvfsumlem4.g | . . . . . 6
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) | 
| 31 | 22, 25, 29, 30 | fvmptf 7037 | . . . . 5
⊢ ((𝑌 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 32 | 1, 21, 31 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 33 |  | dvfsumlem4.1 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑆) | 
| 34 |  | fzfid 14014 | . . . . . . 7
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) | 
| 35 |  | elfzuz 13560 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) | 
| 36 | 35, 6 | eleqtrrdi 2852 | . . . . . . . 8
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) | 
| 37 | 4, 36, 10 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ) | 
| 38 | 34, 37 | fsumrecl 15770 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ) | 
| 39 |  | nfcsb1v 3923 | . . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 | 
| 40 | 39 | nfel1 2922 | . . . . . . . 8
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ | 
| 41 |  | csbeq1a 3913 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → 𝐴 = ⦋𝑋 / 𝑥⦌𝐴) | 
| 42 | 41 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 43 | 40, 42 | rspc 3610 | . . . . . . 7
⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 44 | 33, 14, 43 | sylc 65 | . . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ) | 
| 45 | 38, 44 | resubcld 11691 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) | 
| 46 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑥𝑋 | 
| 47 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 | 
| 48 | 47, 24, 39 | nfov 7461 | . . . . . 6
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) | 
| 49 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋)) | 
| 50 | 49 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋))) | 
| 51 | 50 | sumeq1d 15736 | . . . . . . 7
⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) | 
| 52 | 51, 41 | oveq12d 7449 | . . . . . 6
⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) | 
| 53 | 46, 48, 52, 30 | fvmptf 7037 | . . . . 5
⊢ ((𝑋 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) | 
| 54 | 33, 45, 53 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) | 
| 55 | 32, 54 | oveq12d 7449 | . . 3
⊢ (𝜑 → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 56 | 55 | fveq2d 6910 | . 2
⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) | 
| 57 |  | dvfsum.s | . . . . . . . . . . 11
⊢ 𝑆 = (𝑇(,)+∞) | 
| 58 |  | ioossre 13448 | . . . . . . . . . . 11
⊢ (𝑇(,)+∞) ⊆
ℝ | 
| 59 | 57, 58 | eqsstri 4030 | . . . . . . . . . 10
⊢ 𝑆 ⊆
ℝ | 
| 60 | 59 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℝ) | 
| 61 |  | dvfsum.b1 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) | 
| 62 |  | dvfsum.b3 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) | 
| 63 | 60, 13, 61, 62 | dvmptrecl 26064 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) | 
| 64 | 63 | ralrimiva 3146 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ) | 
| 65 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑚 𝐵 ∈ ℝ | 
| 66 |  | nfcsb1v 3923 | . . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 | 
| 67 | 66 | nfel1 2922 | . . . . . . . 8
⊢
Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ | 
| 68 |  | csbeq1a 3913 | . . . . . . . . 9
⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵) | 
| 69 | 68 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 70 | 65, 67, 69 | cbvralw 3306 | . . . . . . 7
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ ℝ ↔ ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ) | 
| 71 | 64, 70 | sylib 218 | . . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ) | 
| 72 |  | csbeq1 3902 | . . . . . . . 8
⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵) | 
| 73 | 72 | eleq1d 2826 | . . . . . . 7
⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 74 | 73 | rspcv 3618 | . . . . . 6
⊢ (𝑋 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 75 | 33, 71, 74 | sylc 65 | . . . . 5
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) | 
| 76 | 45, 75 | resubcld 11691 | . . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) | 
| 77 | 59, 33 | sselid 3981 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 78 |  | reflcl 13836 | . . . . . . . . 9
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) | 
| 79 | 77, 78 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) | 
| 80 | 77, 79 | resubcld 11691 | . . . . . . 7
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ) | 
| 81 | 80, 75 | remulcld 11291 | . . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) | 
| 82 | 81, 45 | readdcld 11290 | . . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) | 
| 83 | 82, 75 | resubcld 11691 | . . . 4
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) | 
| 84 |  | fracge0 13844 | . . . . . . . 8
⊢ (𝑋 ∈ ℝ → 0 ≤
(𝑋 −
(⌊‘𝑋))) | 
| 85 | 77, 84 | syl 17 | . . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋))) | 
| 86 |  | dvfsumlem4.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ≤ 𝑋) | 
| 87 | 77 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈
ℝ*) | 
| 88 | 59, 1 | sselid 3981 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 89 | 88 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈
ℝ*) | 
| 90 |  | dvfsum.u | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈
ℝ*) | 
| 91 |  | dvfsumlem4.4 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≤ 𝑌) | 
| 92 |  | dvfsumlem4.5 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ≤ 𝑈) | 
| 93 | 87, 89, 90, 91, 92 | xrletrd 13204 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ 𝑈) | 
| 94 | 33, 86, 93 | 3jca 1129 | . . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) | 
| 95 |  | simpr1 1195 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) → 𝑋 ∈ 𝑆) | 
| 96 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) | 
| 97 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥0 | 
| 98 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥
≤ | 
| 99 |  | nfcsb1v 3923 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 | 
| 100 | 97, 98, 99 | nfbr 5190 | . . . . . . . . . . 11
⊢
Ⅎ𝑥0 ≤
⦋𝑋 / 𝑥⦌𝐵 | 
| 101 | 96, 100 | nfim 1896 | . . . . . . . . . 10
⊢
Ⅎ𝑥((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵) | 
| 102 |  | eleq1 2829 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆)) | 
| 103 |  | breq2 5147 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋)) | 
| 104 |  | breq1 5146 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑈 ↔ 𝑋 ≤ 𝑈)) | 
| 105 | 102, 103,
104 | 3anbi123d 1438 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈) ↔ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈))) | 
| 106 | 105 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)))) | 
| 107 |  | csbeq1a 3913 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) | 
| 108 | 107 | breq2d 5155 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)) | 
| 109 | 106, 108 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))) | 
| 110 |  | dvfsumlem4.0 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵) | 
| 111 | 101, 109,
110 | vtoclg1f 3570 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑆 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)) | 
| 112 | 95, 111 | mpcom 38 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈)) → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵) | 
| 113 | 94, 112 | mpdan 687 | . . . . . . 7
⊢ (𝜑 → 0 ≤
⦋𝑋 / 𝑥⦌𝐵) | 
| 114 | 80, 75, 85, 113 | mulge0d 11840 | . . . . . 6
⊢ (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) | 
| 115 | 45, 81 | addge02d 11852 | . . . . . 6
⊢ (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) | 
| 116 | 114, 115 | mpbid 232 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 117 | 45, 82, 75, 116 | lesub1dd 11879 | . . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵)) | 
| 118 |  | reflcl 13836 | . . . . . . . . . 10
⊢ (𝑌 ∈ ℝ →
(⌊‘𝑌) ∈
ℝ) | 
| 119 | 88, 118 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (⌊‘𝑌) ∈
ℝ) | 
| 120 | 88, 119 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ) | 
| 121 |  | csbeq1 3902 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑌 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) | 
| 122 | 121 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑚 = 𝑌 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 123 | 122 | rspcv 3618 | . . . . . . . . 9
⊢ (𝑌 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 124 | 1, 71, 123 | sylc 65 | . . . . . . . 8
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) | 
| 125 | 120, 124 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) | 
| 126 | 125, 21 | readdcld 11290 | . . . . . 6
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) | 
| 127 | 126, 124 | resubcld 11691 | . . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) | 
| 128 |  | dvfsum.m | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 129 |  | dvfsum.d | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 130 |  | dvfsum.md | . . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) | 
| 131 |  | dvfsum.t | . . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 132 |  | dvfsum.l | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) | 
| 133 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) | 
| 134 | 57, 6, 128, 129, 130, 131, 13, 61, 3, 62, 8, 90, 132, 133, 33, 1, 86, 91, 92 | dvfsumlem3 26069 | . . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋) ∧ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) | 
| 135 | 134 | simprd 495 | . . . . . 6
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)) | 
| 136 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑋 − (⌊‘𝑋)) | 
| 137 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑥
· | 
| 138 | 136, 137,
99 | nfov 7461 | . . . . . . . . . 10
⊢
Ⅎ𝑥((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) | 
| 139 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑥
+ | 
| 140 | 138, 139,
48 | nfov 7461 | . . . . . . . . 9
⊢
Ⅎ𝑥(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) | 
| 141 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) | 
| 142 | 141, 49 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋))) | 
| 143 | 142, 107 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · 𝐵) = ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) | 
| 144 | 143, 52 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 145 | 46, 140, 144, 133 | fvmptf 7037 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 146 | 33, 82, 145 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 147 | 146 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵)) | 
| 148 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑌 − (⌊‘𝑌)) | 
| 149 |  | nfcsb1v 3923 | . . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐵 | 
| 150 | 148, 137,
149 | nfov 7461 | . . . . . . . . . 10
⊢
Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) | 
| 151 | 150, 139,
25 | nfov 7461 | . . . . . . . . 9
⊢
Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 152 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌) | 
| 153 | 152, 26 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌))) | 
| 154 |  | csbeq1a 3913 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → 𝐵 = ⦋𝑌 / 𝑥⦌𝐵) | 
| 155 | 153, 154 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · 𝐵) = ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) | 
| 156 | 155, 29 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) | 
| 157 | 22, 151, 156, 133 | fvmptf 7037 | . . . . . . . 8
⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) | 
| 158 | 1, 126, 157 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) | 
| 159 | 158 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − ⦋𝑌 / 𝑥⦌𝐵)) | 
| 160 | 135, 147,
159 | 3brtr3d 5174 | . . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − ⦋𝑌 / 𝑥⦌𝐵)) | 
| 161 | 21 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) | 
| 162 | 124 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) | 
| 163 | 125 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) | 
| 164 | 161, 162,
163 | subsub3d 11650 | . . . . . . 7
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵))) = (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) − ⦋𝑌 / 𝑥⦌𝐵)) | 
| 165 | 161, 163 | addcomd 11463 | . . . . . . . 8
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) | 
| 166 | 165 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) − ⦋𝑌 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − ⦋𝑌 / 𝑥⦌𝐵)) | 
| 167 | 164, 166 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵))) = ((((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − ⦋𝑌 / 𝑥⦌𝐵)) | 
| 168 |  | 1red 11262 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) | 
| 169 | 129, 77, 88, 86, 91 | letrd 11418 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ≤ 𝑌) | 
| 170 | 1, 169, 92 | 3jca 1129 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) | 
| 171 |  | simpr1 1195 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 𝑌 ∈ 𝑆) | 
| 172 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) | 
| 173 | 97, 98, 149 | nfbr 5190 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥0 ≤
⦋𝑌 / 𝑥⦌𝐵 | 
| 174 | 172, 173 | nfim 1896 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 0 ≤ ⦋𝑌 / 𝑥⦌𝐵) | 
| 175 |  | eleq1 2829 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (𝑥 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆)) | 
| 176 |  | breq2 5147 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌)) | 
| 177 |  | breq1 5146 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (𝑥 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈)) | 
| 178 | 175, 176,
177 | 3anbi123d 1438 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → ((𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈) ↔ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈))) | 
| 179 | 178 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)))) | 
| 180 | 154 | breq2d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑌 / 𝑥⦌𝐵)) | 
| 181 | 179, 180 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑌 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈)) → 0 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 0 ≤ ⦋𝑌 / 𝑥⦌𝐵))) | 
| 182 | 174, 181,
110 | vtoclg1f 3570 | . . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝑆 → ((𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 0 ≤ ⦋𝑌 / 𝑥⦌𝐵)) | 
| 183 | 171, 182 | mpcom 38 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 0 ≤ ⦋𝑌 / 𝑥⦌𝐵) | 
| 184 | 170, 183 | mpdan 687 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤
⦋𝑌 / 𝑥⦌𝐵) | 
| 185 |  | fracle1 13843 | . . . . . . . . . . 11
⊢ (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1) | 
| 186 | 88, 185 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1) | 
| 187 | 120, 168,
124, 184, 186 | lemul1ad 12207 | . . . . . . . . 9
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑌 / 𝑥⦌𝐵)) | 
| 188 | 162 | mullidd 11279 | . . . . . . . . 9
⊢ (𝜑 → (1 ·
⦋𝑌 / 𝑥⦌𝐵) = ⦋𝑌 / 𝑥⦌𝐵) | 
| 189 | 187, 188 | breqtrd 5169 | . . . . . . . 8
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ ⦋𝑌 / 𝑥⦌𝐵) | 
| 190 | 124, 125 | subge0d 11853 | . . . . . . . 8
⊢ (𝜑 → (0 ≤
(⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) ↔ ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ ⦋𝑌 / 𝑥⦌𝐵)) | 
| 191 | 189, 190 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → 0 ≤
(⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵))) | 
| 192 | 124, 125 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) ∈ ℝ) | 
| 193 | 21, 192 | subge02d 11855 | . . . . . . 7
⊢ (𝜑 → (0 ≤
(⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) ↔ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵))) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) | 
| 194 | 191, 193 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (⦋𝑌 / 𝑥⦌𝐵 − ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵))) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 195 | 167, 194 | eqbrtrrd 5167 | . . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − ⦋𝑌 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 196 | 83, 127, 21, 160, 195 | letrd 11418 | . . . 4
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 197 | 76, 83, 21, 117, 196 | letrd 11418 | . . 3
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) | 
| 198 | 75, 45 | readdcld 11290 | . . . . 5
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) | 
| 199 |  | fracge0 13844 | . . . . . . . . 9
⊢ (𝑌 ∈ ℝ → 0 ≤
(𝑌 −
(⌊‘𝑌))) | 
| 200 | 88, 199 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌))) | 
| 201 | 120, 124,
200, 184 | mulge0d 11840 | . . . . . . 7
⊢ (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) | 
| 202 | 21, 125 | addge02d 11852 | . . . . . . 7
⊢ (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) | 
| 203 | 201, 202 | mpbid 232 | . . . . . 6
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) | 
| 204 | 134 | simpld 494 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)))‘𝑋)) | 
| 205 | 204, 158,
146 | 3brtr3d 5174 | . . . . . 6
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 206 | 21, 126, 82, 203, 205 | letrd 11418 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 207 |  | fracle1 13843 | . . . . . . . . 9
⊢ (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1) | 
| 208 | 77, 207 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1) | 
| 209 | 80, 168, 75, 113, 208 | lemul1ad 12207 | . . . . . . 7
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑋 / 𝑥⦌𝐵)) | 
| 210 | 75 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) | 
| 211 | 210 | mullidd 11279 | . . . . . . 7
⊢ (𝜑 → (1 ·
⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵) | 
| 212 | 209, 211 | breqtrd 5169 | . . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ ⦋𝑋 / 𝑥⦌𝐵) | 
| 213 | 81, 75, 45, 212 | leadd1dd 11877 | . . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 214 | 21, 82, 198, 206, 213 | letrd 11418 | . . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) | 
| 215 | 45 | recnd 11289 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ) | 
| 216 | 210, 215 | addcomd 11463 | . . . 4
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) + ⦋𝑋 / 𝑥⦌𝐵)) | 
| 217 | 214, 216 | breqtrd 5169 | . . 3
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) + ⦋𝑋 / 𝑥⦌𝐵)) | 
| 218 | 21, 45, 75 | absdifled 15473 | . . 3
⊢ (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ ⦋𝑋 / 𝑥⦌𝐵 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) + ⦋𝑋 / 𝑥⦌𝐵)))) | 
| 219 | 197, 217,
218 | mpbir2and 713 | . 2
⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ ⦋𝑋 / 𝑥⦌𝐵) | 
| 220 | 56, 219 | eqbrtrd 5165 | 1
⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐵) |