Step | Hyp | Ref
| Expression |
1 | | dvfsum2.2 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
2 | | fzfid 13375 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...(⌊‘𝑌)) ∈ Fin) |
3 | | dvfsum2.b2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
4 | 3 | ralrimiva 3111 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ) |
5 | | elfzuz 12937 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
6 | | dvfsum2.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
7 | 5, 6 | eleqtrrdi 2862 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑌)) → 𝑘 ∈ 𝑍) |
8 | | dvfsum2.c |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
9 | 8 | eleq1d 2835 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
10 | 9 | rspccva 3538 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ) |
11 | 4, 7, 10 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℝ) |
12 | 2, 11 | fsumrecl 15124 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℝ) |
13 | | dvfsum2.a |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
14 | 13 | ralrimiva 3111 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ) |
15 | | nfcsb1v 3825 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 |
16 | 15 | nfel1 2933 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ |
17 | | csbeq1a 3815 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴) |
18 | 17 | eleq1d 2835 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
19 | 16, 18 | rspc 3527 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
20 | 1, 14, 19 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ) |
21 | 12, 20 | resubcld 11091 |
. . . . . 6
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
22 | | nfcv 2917 |
. . . . . . 7
⊢
Ⅎ𝑥𝑌 |
23 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 |
24 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑥
− |
25 | 23, 24, 15 | nfov 7173 |
. . . . . . 7
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) |
26 | | fveq2 6651 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌)) |
27 | 26 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌))) |
28 | 27 | sumeq1d 15091 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶) |
29 | 28, 17 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
30 | | dvfsum2.g |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) |
31 | 22, 25, 29, 30 | fvmptf 6773 |
. . . . . 6
⊢ ((𝑌 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
32 | 1, 21, 31 | syl2anc 588 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑌) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
33 | | dvfsum2.1 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
34 | | fzfid 13375 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) |
35 | | elfzuz 12937 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
36 | 35, 6 | eleqtrrdi 2862 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) |
37 | 4, 36, 10 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ) |
38 | 34, 37 | fsumrecl 15124 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ) |
39 | | nfcsb1v 3825 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 |
40 | 39 | nfel1 2933 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ |
41 | | csbeq1a 3815 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → 𝐴 = ⦋𝑋 / 𝑥⦌𝐴) |
42 | 41 | eleq1d 2835 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
43 | 40, 42 | rspc 3527 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
44 | 33, 14, 43 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ) |
45 | 38, 44 | resubcld 11091 |
. . . . . 6
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
46 | | nfcv 2917 |
. . . . . . 7
⊢
Ⅎ𝑥𝑋 |
47 | | nfcv 2917 |
. . . . . . . 8
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 |
48 | 47, 24, 39 | nfov 7173 |
. . . . . . 7
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) |
49 | | fveq2 6651 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (⌊‘𝑥) = (⌊‘𝑋)) |
50 | 49 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑋))) |
51 | 50 | sumeq1d 15091 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) |
52 | 51, 41 | oveq12d 7161 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) |
53 | 46, 48, 52, 30 | fvmptf 6773 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑆 ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) |
54 | 33, 45, 53 | syl2anc 588 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑋) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) |
55 | 32, 54 | oveq12d 7161 |
. . . 4
⊢ (𝜑 → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
56 | 55 | fveq2d 6655 |
. . 3
⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) |
57 | 21 | recnd 10692 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
58 | 45 | recnd 10692 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ) |
59 | 57, 58 | abssubd 14846 |
. . 3
⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) |
60 | 56, 59 | eqtrd 2794 |
. 2
⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) = (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) |
61 | | dvfsum2.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝑇(,)+∞) |
62 | | ioossre 12825 |
. . . . . . . . . 10
⊢ (𝑇(,)+∞) ⊆
ℝ |
63 | 61, 62 | eqsstri 3922 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℝ |
64 | 63 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
65 | | dvfsum2.b1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
66 | | dvfsum2.b3 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
67 | 64, 13, 65, 66 | dvmptrecl 24708 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
68 | 67 | ralrimiva 3111 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ) |
69 | | dvfsum2.e |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → 𝐵 = 𝐸) |
70 | 69 | eleq1d 2835 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ)) |
71 | 70 | rspcv 3534 |
. . . . . 6
⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ)) |
72 | 1, 68, 71 | sylc 65 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) |
73 | 21, 72 | resubcld 11091 |
. . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ∈ ℝ) |
74 | 63, 33 | sseldi 3886 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
75 | | reflcl 13200 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) |
77 | 74, 76 | resubcld 11091 |
. . . . . . 7
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ) |
78 | | nfv 1916 |
. . . . . . . . . 10
⊢
Ⅎ𝑚 𝐵 ∈ ℝ |
79 | | nfcsb1v 3825 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 |
80 | 79 | nfel1 2933 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ |
81 | | csbeq1a 3815 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵) |
82 | 81 | eleq1d 2835 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑚 → (𝐵 ∈ ℝ ↔ ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ)) |
83 | 78, 80, 82 | cbvralw 3350 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ ℝ ↔ ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ) |
84 | 68, 83 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ) |
85 | | csbeq1 3804 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
86 | 85 | eleq1d 2835 |
. . . . . . . . 9
⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
87 | 86 | rspcv 3534 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑆 → (∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
88 | 33, 84, 87 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
89 | 77, 88 | remulcld 10694 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
90 | 89, 45 | readdcld 10693 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) |
91 | 90, 88 | resubcld 11091 |
. . . 4
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
92 | 63, 1 | sseldi 3886 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℝ) |
93 | | reflcl 13200 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℝ →
(⌊‘𝑌) ∈
ℝ) |
94 | 92, 93 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘𝑌) ∈
ℝ) |
95 | 92, 94 | resubcld 11091 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℝ) |
96 | 95, 72 | remulcld 10694 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℝ) |
97 | 96, 21 | readdcld 10693 |
. . . . . 6
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) |
98 | 97, 72 | resubcld 11091 |
. . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ∈ ℝ) |
99 | | fracge0 13208 |
. . . . . . . . 9
⊢ (𝑌 ∈ ℝ → 0 ≤
(𝑌 −
(⌊‘𝑌))) |
100 | 92, 99 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝑌 − (⌊‘𝑌))) |
101 | | dvfsum2.0 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) |
102 | 101 | expr 461 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 0 ≤ 𝐵)) |
103 | 102 | ralrimiva 3111 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵)) |
104 | | dvfsum2.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℝ) |
105 | | dvfsum2.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
106 | | dvfsum2.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
107 | 104, 74, 92, 105, 106 | letrd 10820 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ≤ 𝑌) |
108 | | breq2 5029 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌)) |
109 | 69 | breq2d 5037 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (0 ≤ 𝐵 ↔ 0 ≤ 𝐸)) |
110 | 108, 109 | imbi12d 349 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑌 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑌 → 0 ≤ 𝐸))) |
111 | 110 | rspcv 3534 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑌 → 0 ≤ 𝐸))) |
112 | 1, 103, 107, 111 | syl3c 66 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝐸) |
113 | 95, 72, 100, 112 | mulge0d 11240 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸)) |
114 | 21, 96 | addge02d 11252 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ ((𝑌 − (⌊‘𝑌)) · 𝐸) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) |
115 | 113, 114 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
116 | 21, 97, 72, 115 | lesub1dd 11279 |
. . . . 5
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸)) |
117 | | dvfsum2.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
118 | | dvfsum2.md |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
119 | | dvfsum2.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℝ) |
120 | 13 | renegcld 11090 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐴 ∈ ℝ) |
121 | 67 | renegcld 11090 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -𝐵 ∈ ℝ) |
122 | 3 | renegcld 11090 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → -𝐵 ∈ ℝ) |
123 | | reelprrecn 10652 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
125 | 13 | recnd 10692 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
126 | 124, 125,
65, 66 | dvmptneg 24650 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ -𝐴)) = (𝑥 ∈ 𝑆 ↦ -𝐵)) |
127 | 8 | negeqd 10903 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → -𝐵 = -𝐶) |
128 | | dvfsum2.u |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
129 | | dvfsum2.l |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ≤ 𝐶) |
130 | 67 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆)) → 𝐵 ∈ ℝ) |
131 | 130 | 3adant3 1130 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐵 ∈ ℝ) |
132 | | simp2r 1198 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑘 ∈ 𝑆) |
133 | 68 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ) |
134 | 9 | rspcv 3534 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ)) |
135 | 132, 133,
134 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ∈ ℝ) |
136 | 131, 135 | lenegd 11242 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → (𝐵 ≤ 𝐶 ↔ -𝐶 ≤ -𝐵)) |
137 | 129, 136 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → -𝐶 ≤ -𝐵) |
138 | | eqid 2759 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴))) = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴))) |
139 | | dvfsum2.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ≤ 𝑈) |
140 | 61, 6, 117, 104, 118, 119, 120, 121, 122, 126, 127, 128, 137, 138, 33, 1, 105, 106, 139 | dvfsumlem3 24712 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) ∧ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵))) |
141 | 140 | simprd 500 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) ≤ (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵)) |
142 | 77 | recnd 10692 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ) |
143 | 88 | recnd 10692 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
144 | 142, 143 | mulneg2d 11117 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) = -((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) |
145 | 38 | recnd 10692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ) |
146 | 44 | recnd 10692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ) |
147 | 145, 146 | neg2subd 11037 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
148 | 37 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ) |
149 | 34, 148 | fsumneg 15175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) |
150 | 149 | oveq1d 7158 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) |
151 | 145, 146 | negsubdi2d 11036 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) = (⦋𝑋 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
152 | 147, 150,
151 | 3eqtr4d 2804 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) |
153 | 144, 152 | oveq12d 7161 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
154 | 89 | recnd 10692 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
155 | 154, 58 | negdid 11033 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) = (-((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
156 | 153, 155 | eqtr4d 2797 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
157 | 90 | renegcld 11090 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) |
158 | 156, 157 | eqeltrd 2851 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) |
159 | | nfcv 2917 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑋 − (⌊‘𝑋)) |
160 | | nfcv 2917 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥
· |
161 | | nfcsb1v 3825 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 |
162 | 161 | nfneg 10905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐵 |
163 | 159, 160,
162 | nfov 7173 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) |
164 | | nfcv 2917 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥
+ |
165 | | nfcv 2917 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 |
166 | 39 | nfneg 10905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥-⦋𝑋 / 𝑥⦌𝐴 |
167 | 165, 24, 166 | nfov 7173 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴) |
168 | 163, 164,
167 | nfov 7173 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) |
169 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
170 | 169, 49 | oveq12d 7161 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → (𝑥 − (⌊‘𝑥)) = (𝑋 − (⌊‘𝑋))) |
171 | | csbeq1a 3815 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
172 | 171 | negeqd 10903 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → -𝐵 = -⦋𝑋 / 𝑥⦌𝐵) |
173 | 170, 172 | oveq12d 7161 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵)) |
174 | 50 | sumeq1d 15091 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶) |
175 | 41 | negeqd 10903 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → -𝐴 = -⦋𝑋 / 𝑥⦌𝐴) |
176 | 174, 175 | oveq12d 7161 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) |
177 | 173, 176 | oveq12d 7161 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))) |
178 | 46, 168, 177, 138 | fvmptf 6773 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑆 ∧ (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))) |
179 | 33, 158, 178 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = (((𝑋 − (⌊‘𝑋)) · -⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))-𝐶 − -⦋𝑋 / 𝑥⦌𝐴))) |
180 | 179, 156 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) = -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
181 | | csbnegg 10906 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑆 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵) |
182 | 33, 181 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌-𝐵 = -⦋𝑋 / 𝑥⦌𝐵) |
183 | 180, 182 | oveq12d 7161 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋) − ⦋𝑋 / 𝑥⦌-𝐵) = (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵)) |
184 | 95 | recnd 10692 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ∈ ℂ) |
185 | 72 | recnd 10692 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 ∈ ℂ) |
186 | 184, 185 | mulneg2d 11117 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · -𝐸) = -((𝑌 − (⌊‘𝑌)) · 𝐸)) |
187 | 12 | recnd 10692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 ∈ ℂ) |
188 | 20 | recnd 10692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ) |
189 | 187, 188 | neg2subd 11037 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)) |
190 | 11 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑌))) → 𝐶 ∈ ℂ) |
191 | 2, 190 | fsumneg 15175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 = -Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶) |
192 | 191 | oveq1d 7158 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = (-Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) |
193 | 187, 188 | negsubdi2d 11036 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶)) |
194 | 189, 192,
193 | 3eqtr4d 2804 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) = -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
195 | 186, 194 | oveq12d 7161 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
196 | 96 | recnd 10692 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ∈ ℂ) |
197 | 196, 57 | negdid 11033 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (-((𝑌 − (⌊‘𝑌)) · 𝐸) + -(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
198 | 195, 197 | eqtr4d 2797 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
199 | 97 | renegcld 11090 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) |
200 | 198, 199 | eqeltrd 2851 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) |
201 | | nfcv 2917 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · -𝐸) |
202 | | nfcv 2917 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 |
203 | 15 | nfneg 10905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥-⦋𝑌 / 𝑥⦌𝐴 |
204 | 202, 24, 203 | nfov 7173 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴) |
205 | 201, 164,
204 | nfov 7173 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) |
206 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌) |
207 | 206, 26 | oveq12d 7161 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌))) |
208 | 69 | negeqd 10903 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → -𝐵 = -𝐸) |
209 | 207, 208 | oveq12d 7161 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · -𝐵) = ((𝑌 − (⌊‘𝑌)) · -𝐸)) |
210 | 27 | sumeq1d 15091 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶) |
211 | 17 | negeqd 10903 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → -𝐴 = -⦋𝑌 / 𝑥⦌𝐴) |
212 | 210, 211 | oveq12d 7161 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) |
213 | 209, 212 | oveq12d 7161 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))) |
214 | 22, 205, 213, 138 | fvmptf 6773 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴)) ∈ ℝ) → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))) |
215 | 1, 200, 214 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = (((𝑌 − (⌊‘𝑌)) · -𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))-𝐶 − -⦋𝑌 / 𝑥⦌𝐴))) |
216 | 215, 198 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) = -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
217 | 208 | adantl 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = 𝑌) → -𝐵 = -𝐸) |
218 | 1, 217 | csbied 3837 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌-𝐵 = -𝐸) |
219 | 216, 218 | oveq12d 7161 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) − ⦋𝑌 / 𝑥⦌-𝐵) = (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸)) |
220 | 141, 183,
219 | 3brtr3d 5056 |
. . . . . . . 8
⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) ≤ (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸)) |
221 | 90 | recnd 10692 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ∈ ℂ) |
222 | 221, 143 | neg2subd 11037 |
. . . . . . . 8
⊢ (𝜑 → (-(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − -⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) |
223 | 97 | recnd 10692 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ ℂ) |
224 | 223, 185 | neg2subd 11037 |
. . . . . . . 8
⊢ (𝜑 → (-(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − -𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) |
225 | 220, 222,
224 | 3brtr3d 5056 |
. . . . . . 7
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) ≤ (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) |
226 | 221, 143 | negsubdi2d 11036 |
. . . . . . 7
⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 − (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) |
227 | 223, 185 | negsubdi2d 11036 |
. . . . . . 7
⊢ (𝜑 → -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) = (𝐸 − (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)))) |
228 | 225, 226,
227 | 3brtr4d 5057 |
. . . . . 6
⊢ (𝜑 → -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸)) |
229 | 98, 91 | lenegd 11242 |
. . . . . 6
⊢ (𝜑 → (((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ↔ -((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ -((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸))) |
230 | 228, 229 | mpbird 260 |
. . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵)) |
231 | 73, 98, 91, 116, 230 | letrd 10820 |
. . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵)) |
232 | | 1red 10665 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
233 | | nfv 1916 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝐷 ≤ 𝑋 |
234 | | nfcv 2917 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥0 |
235 | | nfcv 2917 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥
≤ |
236 | 234, 235,
161 | nfbr 5072 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥0 ≤
⦋𝑋 / 𝑥⦌𝐵 |
237 | 233, 236 | nfim 1898 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
238 | | breq2 5029 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋)) |
239 | 171 | breq2d 5037 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (0 ≤ 𝐵 ↔ 0 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
240 | 238, 239 | imbi12d 349 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 → 0 ≤ 𝐵) ↔ (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
241 | 237, 240 | rspc 3527 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 0 ≤ 𝐵) → (𝐷 ≤ 𝑋 → 0 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
242 | 33, 103, 105, 241 | syl3c 66 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤
⦋𝑋 / 𝑥⦌𝐵) |
243 | | fracle1 13207 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ → (𝑋 − (⌊‘𝑋)) ≤ 1) |
244 | 74, 243 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ≤ 1) |
245 | 77, 232, 88, 242, 244 | lemul1ad 11602 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (1 · ⦋𝑋 / 𝑥⦌𝐵)) |
246 | 143 | mulid2d 10682 |
. . . . . . 7
⊢ (𝜑 → (1 ·
⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵) |
247 | 245, 246 | breqtrd 5051 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ≤ ⦋𝑋 / 𝑥⦌𝐵) |
248 | 89, 88, 45, 247 | leadd1dd 11277 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
249 | 90, 88, 45 | lesubadd2d 11262 |
. . . . 5
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ↔ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (⦋𝑋 / 𝑥⦌𝐵 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) |
250 | 248, 249 | mpbird 260 |
. . . 4
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) |
251 | 73, 91, 45, 231, 250 | letrd 10820 |
. . 3
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) |
252 | 21, 72 | readdcld 10693 |
. . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸) ∈ ℝ) |
253 | | fracge0 13208 |
. . . . . . 7
⊢ (𝑋 ∈ ℝ → 0 ≤
(𝑋 −
(⌊‘𝑋))) |
254 | 74, 253 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋))) |
255 | 77, 88, 254, 242 | mulge0d 11240 |
. . . . 5
⊢ (𝜑 → 0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) |
256 | 45, 89 | addge02d 11252 |
. . . . 5
⊢ (𝜑 → (0 ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ↔ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) |
257 | 255, 256 | mpbid 235 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
258 | 140 | simpld 499 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑌) ≤ ((𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · -𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))-𝐶 − -𝐴)))‘𝑋)) |
259 | 258, 216,
180 | 3brtr3d 5056 |
. . . . . 6
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴))) |
260 | 90, 97 | lenegd 11242 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ↔ -(((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ -(((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)))) |
261 | 259, 260 | mpbird 260 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
262 | | fracle1 13207 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℝ → (𝑌 − (⌊‘𝑌)) ≤ 1) |
263 | 92, 262 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − (⌊‘𝑌)) ≤ 1) |
264 | 95, 232, 72, 112, 263 | lemul1ad 11602 |
. . . . . . . 8
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ (1 · 𝐸)) |
265 | 185 | mulid2d 10682 |
. . . . . . . 8
⊢ (𝜑 → (1 · 𝐸) = 𝐸) |
266 | 264, 265 | breqtrd 5051 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 − (⌊‘𝑌)) · 𝐸) ≤ 𝐸) |
267 | 96, 72, 21, 266 | leadd1dd 11277 |
. . . . . 6
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
268 | 185, 57 | addcomd 10865 |
. . . . . 6
⊢ (𝜑 → (𝐸 + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸)) |
269 | 267, 268 | breqtrd 5051 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · 𝐸) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸)) |
270 | 90, 97, 252, 261, 269 | letrd 10820 |
. . . 4
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴)) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸)) |
271 | 45, 90, 252, 257, 270 | letrd 10820 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸)) |
272 | 45, 21, 72 | absdifled 14827 |
. . 3
⊢ (𝜑 → ((abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸 ↔ (((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) − 𝐸) ≤ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ∧ (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + 𝐸)))) |
273 | 251, 271,
272 | mpbir2and 713 |
. 2
⊢ (𝜑 → (abs‘((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑋 / 𝑥⦌𝐴) − (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) ≤ 𝐸) |
274 | 60, 273 | eqbrtrd 5047 |
1
⊢ (𝜑 → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) ≤ 𝐸) |