Metamath Proof Explorer


Theorem dvfsumle

Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses dvfsumle.m φ N M
dvfsumle.a φ x M N A : M N cn
dvfsumle.v φ x M N B V
dvfsumle.b φ dx M N A d x = x M N B
dvfsumle.c x = M A = C
dvfsumle.d x = N A = D
dvfsumle.x φ k M ..^ N X
dvfsumle.l φ k M ..^ N x k k + 1 X B
Assertion dvfsumle φ k M ..^ N X D C

Proof

Step Hyp Ref Expression
1 dvfsumle.m φ N M
2 dvfsumle.a φ x M N A : M N cn
3 dvfsumle.v φ x M N B V
4 dvfsumle.b φ dx M N A d x = x M N B
5 dvfsumle.c x = M A = C
6 dvfsumle.d x = N A = D
7 dvfsumle.x φ k M ..^ N X
8 dvfsumle.l φ k M ..^ N x k k + 1 X B
9 fzofi M ..^ N Fin
10 9 a1i φ M ..^ N Fin
11 eluzel2 N M M
12 1 11 syl φ M
13 eluzelz N M N
14 1 13 syl φ N
15 fzval2 M N M N = M N
16 12 14 15 syl2anc φ M N = M N
17 inss1 M N M N
18 16 17 eqsstrdi φ M N M N
19 18 sselda φ y M N y M N
20 cncff x M N A : M N cn x M N A : M N
21 2 20 syl φ x M N A : M N
22 eqid x M N A = x M N A
23 22 fmpt x M N A x M N A : M N
24 21 23 sylibr φ x M N A
25 nfcsb1v _ x y / x A
26 25 nfel1 x y / x A
27 csbeq1a x = y A = y / x A
28 27 eleq1d x = y A y / x A
29 26 28 rspc y M N x M N A y / x A
30 24 29 mpan9 φ y M N y / x A
31 19 30 syldan φ y M N y / x A
32 31 ralrimiva φ y M N y / x A
33 fzofzp1 k M ..^ N k + 1 M N
34 csbeq1 y = k + 1 y / x A = k + 1 / x A
35 34 eleq1d y = k + 1 y / x A k + 1 / x A
36 35 rspccva y M N y / x A k + 1 M N k + 1 / x A
37 32 33 36 syl2an φ k M ..^ N k + 1 / x A
38 elfzofz k M ..^ N k M N
39 csbeq1 y = k y / x A = k / x A
40 39 eleq1d y = k y / x A k / x A
41 40 rspccva y M N y / x A k M N k / x A
42 32 38 41 syl2an φ k M ..^ N k / x A
43 37 42 resubcld φ k M ..^ N k + 1 / x A k / x A
44 elfzoelz k M ..^ N k
45 44 adantl φ k M ..^ N k
46 45 zred φ k M ..^ N k
47 46 recnd φ k M ..^ N k
48 ax-1cn 1
49 pncan2 k 1 k + 1 - k = 1
50 47 48 49 sylancl φ k M ..^ N k + 1 - k = 1
51 50 oveq2d φ k M ..^ N X k + 1 - k = X 1
52 7 recnd φ k M ..^ N X
53 peano2re k k + 1
54 46 53 syl φ k M ..^ N k + 1
55 54 recnd φ k M ..^ N k + 1
56 52 55 47 subdid φ k M ..^ N X k + 1 - k = X k + 1 X k
57 52 mulridd φ k M ..^ N X 1 = X
58 51 56 57 3eqtr3d φ k M ..^ N X k + 1 X k = X
59 52 adantr φ k M ..^ N y k k + 1 X
60 46 54 iccssred φ k M ..^ N k k + 1
61 ax-resscn
62 60 61 sstrdi φ k M ..^ N k k + 1
63 62 sselda φ k M ..^ N y k k + 1 y
64 ovmpot X y X u , v u v y = X y
65 59 63 64 syl2anc φ k M ..^ N y k k + 1 X u , v u v y = X y
66 65 eqeq2d φ k M ..^ N y k k + 1 z = X u , v u v y z = X y
67 66 pm5.32da φ k M ..^ N y k k + 1 z = X u , v u v y y k k + 1 z = X y
68 67 opabbidv φ k M ..^ N y z | y k k + 1 z = X u , v u v y = y z | y k k + 1 z = X y
69 df-mpt y k k + 1 X y = y z | y k k + 1 z = X y
70 68 69 eqtr4di φ k M ..^ N y z | y k k + 1 z = X u , v u v y = y k k + 1 X y
71 df-mpt y k k + 1 X u , v u v y = y z | y k k + 1 z = X u , v u v y
72 eqid TopOpen fld = TopOpen fld
73 72 mpomulcn u , v u v TopOpen fld × t TopOpen fld Cn TopOpen fld
74 61 a1i φ k M ..^ N
75 cncfmptc X k k + 1 y k k + 1 X : k k + 1 cn
76 7 62 74 75 syl3anc φ k M ..^ N y k k + 1 X : k k + 1 cn
77 cncfmptid k k + 1 y k k + 1 y : k k + 1 cn
78 60 61 77 sylancl φ k M ..^ N y k k + 1 y : k k + 1 cn
79 simpl X y X
80 79 recnd X y X
81 simpr X y y
82 81 recnd X y y
83 64 eqcomd X y X y = X u , v u v y
84 80 82 83 syl2anc X y X y = X u , v u v y
85 remulcl X y X y
86 84 85 eqeltrrd X y X u , v u v y
87 72 73 76 78 61 86 cncfmpt2ss φ k M ..^ N y k k + 1 X u , v u v y : k k + 1 cn
88 71 87 eqeltrrid φ k M ..^ N y z | y k k + 1 z = X u , v u v y : k k + 1 cn
89 70 88 eqeltrrd φ k M ..^ N y k k + 1 X y : k k + 1 cn
90 reelprrecn
91 90 a1i φ k M ..^ N
92 12 zred φ M
93 92 adantr φ k M ..^ N M
94 93 rexrd φ k M ..^ N M *
95 elfzole1 k M ..^ N M k
96 95 adantl φ k M ..^ N M k
97 iooss1 M * M k k k + 1 M k + 1
98 94 96 97 syl2anc φ k M ..^ N k k + 1 M k + 1
99 14 zred φ N
100 99 adantr φ k M ..^ N N
101 100 rexrd φ k M ..^ N N *
102 33 adantl φ k M ..^ N k + 1 M N
103 elfzle2 k + 1 M N k + 1 N
104 102 103 syl φ k M ..^ N k + 1 N
105 iooss2 N * k + 1 N M k + 1 M N
106 101 104 105 syl2anc φ k M ..^ N M k + 1 M N
107 98 106 sstrd φ k M ..^ N k k + 1 M N
108 ioossicc M N M N
109 92 99 iccssred φ M N
110 109 adantr φ k M ..^ N M N
111 110 61 sstrdi φ k M ..^ N M N
112 108 111 sstrid φ k M ..^ N M N
113 107 112 sstrd φ k M ..^ N k k + 1
114 113 sselda φ k M ..^ N y k k + 1 y
115 1cnd φ k M ..^ N y k k + 1 1
116 74 sselda φ k M ..^ N y y
117 1cnd φ k M ..^ N y 1
118 91 dvmptid φ k M ..^ N dy y d y = y 1
119 ioossre k k + 1
120 119 a1i φ k M ..^ N k k + 1
121 72 tgioo2 topGen ran . = TopOpen fld 𝑡
122 iooretop k k + 1 topGen ran .
123 122 a1i φ k M ..^ N k k + 1 topGen ran .
124 91 116 117 118 120 121 72 123 dvmptres φ k M ..^ N dy k k + 1 y d y = y k k + 1 1
125 91 114 115 124 52 dvmptcmul φ k M ..^ N dy k k + 1 X y d y = y k k + 1 X 1
126 57 mpteq2dv φ k M ..^ N y k k + 1 X 1 = y k k + 1 X
127 125 126 eqtrd φ k M ..^ N dy k k + 1 X y d y = y k k + 1 X
128 nfcv _ y A
129 128 25 27 cbvmpt x k k + 1 A = y k k + 1 y / x A
130 iccss M N M k k + 1 N k k + 1 M N
131 93 100 96 104 130 syl22anc φ k M ..^ N k k + 1 M N
132 131 resmptd φ k M ..^ N x M N A k k + 1 = x k k + 1 A
133 2 adantr φ k M ..^ N x M N A : M N cn
134 rescncf k k + 1 M N x M N A : M N cn x M N A k k + 1 : k k + 1 cn
135 131 133 134 sylc φ k M ..^ N x M N A k k + 1 : k k + 1 cn
136 132 135 eqeltrrd φ k M ..^ N x k k + 1 A : k k + 1 cn
137 129 136 eqeltrrid φ k M ..^ N y k k + 1 y / x A : k k + 1 cn
138 21 adantr φ k M ..^ N x M N A : M N
139 138 23 sylibr φ k M ..^ N x M N A
140 108 sseli y M N y M N
141 29 impcom x M N A y M N y / x A
142 139 140 141 syl2an φ k M ..^ N y M N y / x A
143 142 recnd φ k M ..^ N y M N y / x A
144 108 sseli x M N x M N
145 21 fvmptelcdm φ x M N A
146 145 adantlr φ k M ..^ N x M N A
147 144 146 sylan2 φ k M ..^ N x M N A
148 147 fmpttd φ k M ..^ N x M N A : M N
149 ioossre M N
150 dvfre x M N A : M N M N dx M N A d x : dom dx M N A d x
151 148 149 150 sylancl φ k M ..^ N dx M N A d x : dom dx M N A d x
152 4 adantr φ k M ..^ N dx M N A d x = x M N B
153 152 dmeqd φ k M ..^ N dom dx M N A d x = dom x M N B
154 3 adantlr φ k M ..^ N x M N B V
155 154 ralrimiva φ k M ..^ N x M N B V
156 dmmptg x M N B V dom x M N B = M N
157 155 156 syl φ k M ..^ N dom x M N B = M N
158 153 157 eqtrd φ k M ..^ N dom dx M N A d x = M N
159 152 158 feq12d φ k M ..^ N dx M N A d x : dom dx M N A d x x M N B : M N
160 151 159 mpbid φ k M ..^ N x M N B : M N
161 eqid x M N B = x M N B
162 161 fmpt x M N B x M N B : M N
163 160 162 sylibr φ k M ..^ N x M N B
164 nfcsb1v _ x y / x B
165 164 nfel1 x y / x B
166 csbeq1a x = y B = y / x B
167 166 eleq1d x = y B y / x B
168 165 167 rspc y M N x M N B y / x B
169 163 168 mpan9 φ k M ..^ N y M N y / x B
170 128 25 27 cbvmpt x M N A = y M N y / x A
171 170 oveq2i dx M N A d x = dy M N y / x A d y
172 nfcv _ y B
173 172 164 166 cbvmpt x M N B = y M N y / x B
174 152 171 173 3eqtr3g φ k M ..^ N dy M N y / x A d y = y M N y / x B
175 91 143 169 174 107 121 72 123 dvmptres φ k M ..^ N dy k k + 1 y / x A d y = y k k + 1 y / x B
176 8 anassrs φ k M ..^ N x k k + 1 X B
177 176 ralrimiva φ k M ..^ N x k k + 1 X B
178 nfcv _ x X
179 nfcv _ x
180 178 179 164 nfbr x X y / x B
181 166 breq2d x = y X B X y / x B
182 180 181 rspc y k k + 1 x k k + 1 X B X y / x B
183 177 182 mpan9 φ k M ..^ N y k k + 1 X y / x B
184 46 rexrd φ k M ..^ N k *
185 54 rexrd φ k M ..^ N k + 1 *
186 46 lep1d φ k M ..^ N k k + 1
187 lbicc2 k * k + 1 * k k + 1 k k k + 1
188 184 185 186 187 syl3anc φ k M ..^ N k k k + 1
189 ubicc2 k * k + 1 * k k + 1 k + 1 k k + 1
190 184 185 186 189 syl3anc φ k M ..^ N k + 1 k k + 1
191 oveq2 y = k X y = X k
192 oveq2 y = k + 1 X y = X k + 1
193 46 54 89 127 137 175 183 188 190 186 191 39 192 34 dvle φ k M ..^ N X k + 1 X k k + 1 / x A k / x A
194 58 193 eqbrtrrd φ k M ..^ N X k + 1 / x A k / x A
195 10 7 43 194 fsumle φ k M ..^ N X k M ..^ N k + 1 / x A k / x A
196 vex y V
197 196 a1i y = M y V
198 eqeq2 y = M x = y x = M
199 198 biimpa y = M x = y x = M
200 199 5 syl y = M x = y A = C
201 197 200 csbied y = M y / x A = C
202 196 a1i y = N y V
203 eqeq2 y = N x = y x = N
204 203 biimpa y = N x = y x = N
205 204 6 syl y = N x = y A = D
206 202 205 csbied y = N y / x A = D
207 31 recnd φ y M N y / x A
208 39 34 201 206 1 207 telfsumo2 φ k M ..^ N k + 1 / x A k / x A = D C
209 195 208 breqtrd φ k M ..^ N X D C