Metamath Proof Explorer


Theorem dvfsumlem3

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Hypotheses dvfsum.s S=T+∞
dvfsum.z Z=M
dvfsum.m φM
dvfsum.d φD
dvfsum.md φMD+1
dvfsum.t φT
dvfsum.a φxSA
dvfsum.b1 φxSBV
dvfsum.b2 φxZB
dvfsum.b3 φdxSAdx=xSB
dvfsum.c x=kB=C
dvfsum.u φU*
dvfsum.l φxSkSDxxkkUCB
dvfsum.h H=xSxxB+k=MxC-A
dvfsumlem1.1 φXS
dvfsumlem1.2 φYS
dvfsumlem1.3 φDX
dvfsumlem1.4 φXY
dvfsumlem1.5 φYU
Assertion dvfsumlem3 φHYHXHXX/xBHYY/xB

Proof

Step Hyp Ref Expression
1 dvfsum.s S=T+∞
2 dvfsum.z Z=M
3 dvfsum.m φM
4 dvfsum.d φD
5 dvfsum.md φMD+1
6 dvfsum.t φT
7 dvfsum.a φxSA
8 dvfsum.b1 φxSBV
9 dvfsum.b2 φxZB
10 dvfsum.b3 φdxSAdx=xSB
11 dvfsum.c x=kB=C
12 dvfsum.u φU*
13 dvfsum.l φxSkSDxxkkUCB
14 dvfsum.h H=xSxxB+k=MxC-A
15 dvfsumlem1.1 φXS
16 dvfsumlem1.2 φYS
17 dvfsumlem1.3 φDX
18 dvfsumlem1.4 φXY
19 dvfsumlem1.5 φYU
20 ioossre T+∞
21 1 20 eqsstri S
22 21 16 sselid φY
23 21 15 sselid φX
24 reflcl XX
25 peano2re XX+1
26 23 24 25 3syl φX+1
27 3 adantr φYX+1M
28 4 adantr φYX+1D
29 5 adantr φYX+1MD+1
30 6 adantr φYX+1T
31 7 adantlr φYX+1xSA
32 8 adantlr φYX+1xSBV
33 9 adantlr φYX+1xZB
34 10 adantr φYX+1dxSAdx=xSB
35 12 adantr φYX+1U*
36 13 3adant1r φYX+1xSkSDxxkkUCB
37 15 adantr φYX+1XS
38 16 adantr φYX+1YS
39 17 adantr φYX+1DX
40 18 adantr φYX+1XY
41 19 adantr φYX+1YU
42 simpr φYX+1YX+1
43 1 2 27 28 29 30 31 32 33 34 11 35 36 14 37 38 39 40 41 42 dvfsumlem2 φYX+1HYHXHXX/xBHYY/xB
44 21 a1i φS
45 44 sselda φxSx
46 reflcl xx
47 45 46 syl φxSx
48 45 47 resubcld φxSxx
49 44 7 8 10 dvmptrecl φxSB
50 48 49 remulcld φxSxxB
51 fzfid φxSMxFin
52 9 ralrimiva φxZB
53 52 adantr φxSxZB
54 elfzuz kMxkM
55 54 2 eleqtrrdi kMxkZ
56 11 eleq1d x=kBC
57 56 rspccva xZBkZC
58 53 55 57 syl2an φxSkMxC
59 51 58 fsumrecl φxSk=MxC
60 59 7 resubcld φxSk=MxCA
61 50 60 readdcld φxSxxB+k=MxC-A
62 61 14 fmptd φH:S
63 62 adantr φX+1YH:S
64 16 adantr φX+1YYS
65 63 64 ffvelrnd φX+1YHY
66 22 adantr φX+1YY
67 reflcl YY
68 66 67 syl φX+1YY
69 6 adantr φX+1YT
70 23 adantr φX+1YX
71 70 24 25 3syl φX+1YX+1
72 15 1 eleqtrdi φXT+∞
73 6 rexrd φT*
74 elioopnf T*XT+∞XT<X
75 73 74 syl φXT+∞XT<X
76 72 75 mpbid φXT<X
77 76 simprd φT<X
78 fllep1 XXX+1
79 23 78 syl φXX+1
80 6 23 26 77 79 ltletrd φT<X+1
81 80 adantr φX+1YT<X+1
82 simpr φX+1YX+1Y
83 70 flcld φX+1YX
84 83 peano2zd φX+1YX+1
85 flge YX+1X+1YX+1Y
86 66 84 85 syl2anc φX+1YX+1YX+1Y
87 82 86 mpbid φX+1YX+1Y
88 69 71 68 81 87 ltletrd φX+1YT<Y
89 73 adantr φX+1YT*
90 elioopnf T*YT+∞YT<Y
91 89 90 syl φX+1YYT+∞YT<Y
92 68 88 91 mpbir2and φX+1YYT+∞
93 92 1 eleqtrrdi φX+1YYS
94 63 93 ffvelrnd φX+1YHY
95 15 adantr φX+1YXS
96 63 95 ffvelrnd φX+1YHX
97 3 adantr φX+1YM
98 4 adantr φX+1YD
99 5 adantr φX+1YMD+1
100 7 adantlr φX+1YxSA
101 8 adantlr φX+1YxSBV
102 9 adantlr φX+1YxZB
103 10 adantr φX+1YdxSAdx=xSB
104 12 adantr φX+1YU*
105 13 3adant1r φX+1YxSkSDxxkkUCB
106 17 adantr φX+1YDX
107 70 78 syl φX+1YXX+1
108 98 70 71 106 107 letrd φX+1YDX+1
109 98 71 68 108 87 letrd φX+1YDY
110 flle YYY
111 66 110 syl φX+1YYY
112 19 adantr φX+1YYU
113 fllep1 YYY+1
114 66 113 syl φX+1YYY+1
115 flidm YY=Y
116 66 115 syl φX+1YY=Y
117 116 oveq1d φX+1YY+1=Y+1
118 114 117 breqtrrd φX+1YYY+1
119 1 2 97 98 99 69 100 101 102 103 11 104 105 14 93 64 109 111 112 118 dvfsumlem2 φX+1YHYHYHYY/xBHYY/xB
120 119 simpld φX+1YHYHY
121 elioopnf T*X+1T+∞X+1T<X+1
122 73 121 syl φX+1T+∞X+1T<X+1
123 26 80 122 mpbir2and φX+1T+∞
124 123 1 eleqtrrdi φX+1S
125 124 adantr φX+1YX+1S
126 63 125 ffvelrnd φX+1YHX+1
127 66 flcld φX+1YY
128 eluz2 YX+1X+1YX+1Y
129 84 127 87 128 syl3anbrc φX+1YYX+1
130 63 adantr φX+1YmX+1YH:S
131 elfzelz mX+1Ym
132 131 adantl φX+1YmX+1Ym
133 132 zred φX+1YmX+1Ym
134 69 adantr φX+1YmX+1YT
135 71 adantr φX+1YmX+1YX+1
136 80 ad2antrr φX+1YmX+1YT<X+1
137 elfzle1 mX+1YX+1m
138 137 adantl φX+1YmX+1YX+1m
139 134 135 133 136 138 ltletrd φX+1YmX+1YT<m
140 73 ad2antrr φX+1YmX+1YT*
141 elioopnf T*mT+∞mT<m
142 140 141 syl φX+1YmX+1YmT+∞mT<m
143 133 139 142 mpbir2and φX+1YmX+1YmT+∞
144 143 1 eleqtrrdi φX+1YmX+1YmS
145 130 144 ffvelrnd φX+1YmX+1YHm
146 97 adantr φX+1YmX+1Y1M
147 98 adantr φX+1YmX+1Y1D
148 5 ad2antrr φX+1YmX+1Y1MD+1
149 69 adantr φX+1YmX+1Y1T
150 100 adantlr φX+1YmX+1Y1xSA
151 101 adantlr φX+1YmX+1Y1xSBV
152 102 adantlr φX+1YmX+1Y1xZB
153 103 adantr φX+1YmX+1Y1dxSAdx=xSB
154 104 adantr φX+1YmX+1Y1U*
155 105 3adant1r φX+1YmX+1Y1xSkSDxxkkUCB
156 elfzelz mX+1Y1m
157 156 adantl φX+1YmX+1Y1m
158 157 zred φX+1YmX+1Y1m
159 71 adantr φX+1YmX+1Y1X+1
160 80 ad2antrr φX+1YmX+1Y1T<X+1
161 elfzle1 mX+1Y1X+1m
162 161 adantl φX+1YmX+1Y1X+1m
163 149 159 158 160 162 ltletrd φX+1YmX+1Y1T<m
164 149 rexrd φX+1YmX+1Y1T*
165 164 141 syl φX+1YmX+1Y1mT+∞mT<m
166 158 163 165 mpbir2and φX+1YmX+1Y1mT+∞
167 166 1 eleqtrrdi φX+1YmX+1Y1mS
168 peano2re mm+1
169 158 168 syl φX+1YmX+1Y1m+1
170 158 lep1d φX+1YmX+1Y1mm+1
171 149 158 169 163 170 ltletrd φX+1YmX+1Y1T<m+1
172 elioopnf T*m+1T+∞m+1T<m+1
173 164 172 syl φX+1YmX+1Y1m+1T+∞m+1T<m+1
174 169 171 173 mpbir2and φX+1YmX+1Y1m+1T+∞
175 174 1 eleqtrrdi φX+1YmX+1Y1m+1S
176 108 adantr φX+1YmX+1Y1DX+1
177 147 159 158 176 162 letrd φX+1YmX+1Y1Dm
178 169 rexrd φX+1YmX+1Y1m+1*
179 68 rexrd φX+1YY*
180 179 adantr φX+1YmX+1Y1Y*
181 elfzle2 mX+1Y1mY1
182 181 adantl φX+1YmX+1Y1mY1
183 1red φX+1YmX+1Y11
184 66 adantr φX+1YmX+1Y1Y
185 184 67 syl φX+1YmX+1Y1Y
186 leaddsub m1Ym+1YmY1
187 158 183 185 186 syl3anc φX+1YmX+1Y1m+1YmY1
188 182 187 mpbird φX+1YmX+1Y1m+1Y
189 66 rexrd φX+1YY*
190 179 189 104 111 112 xrletrd φX+1YYU
191 190 adantr φX+1YmX+1Y1YU
192 178 180 154 188 191 xrletrd φX+1YmX+1Y1m+1U
193 flid mm=m
194 157 193 syl φX+1YmX+1Y1m=m
195 194 eqcomd φX+1YmX+1Y1m=m
196 195 oveq1d φX+1YmX+1Y1m+1=m+1
197 169 196 eqled φX+1YmX+1Y1m+1m+1
198 1 2 146 147 148 149 150 151 152 153 11 154 155 14 167 175 177 170 192 197 dvfsumlem2 φX+1YmX+1Y1Hm+1HmHmm/xBHm+1m+1/xB
199 198 simpld φX+1YmX+1Y1Hm+1Hm
200 129 145 199 monoord2 φX+1YHYHX+1
201 71 rexrd φX+1YX+1*
202 201 179 104 87 190 xrletrd φX+1YX+1U
203 71 leidd φX+1YX+1X+1
204 1 2 97 98 99 69 100 101 102 103 11 104 105 14 95 125 106 107 202 203 dvfsumlem2 φX+1YHX+1HXHXX/xBHX+1X+1/xB
205 204 simpld φX+1YHX+1HX
206 94 126 96 200 205 letrd φX+1YHYHX
207 65 94 96 120 206 letrd φX+1YHYHX
208 csbeq1 m=Xm/xB=X/xB
209 208 eleq1d m=Xm/xBX/xB
210 49 ralrimiva φxSB
211 210 adantr φX+1YxSB
212 nfcsb1v _xm/xB
213 212 nfel1 xm/xB
214 csbeq1a x=mB=m/xB
215 214 eleq1d x=mBm/xB
216 213 215 rspc mSxSBm/xB
217 211 216 mpan9 φX+1YmSm/xB
218 217 ralrimiva φX+1YmSm/xB
219 209 218 95 rspcdva φX+1YX/xB
220 96 219 resubcld φX+1YHXX/xB
221 csbeq1 m=Ym/xB=Y/xB
222 221 eleq1d m=Ym/xBY/xB
223 222 218 93 rspcdva φX+1YY/xB
224 94 223 resubcld φX+1YHYY/xB
225 csbeq1 m=Ym/xB=Y/xB
226 225 eleq1d m=Ym/xBY/xB
227 226 218 64 rspcdva φX+1YY/xB
228 65 227 resubcld φX+1YHYY/xB
229 csbeq1 m=X+1m/xB=X+1/xB
230 229 eleq1d m=X+1m/xBX+1/xB
231 230 218 125 rspcdva φX+1YX+1/xB
232 126 231 resubcld φX+1YHX+1X+1/xB
233 204 simprd φX+1YHXX/xBHX+1X+1/xB
234 fveq2 y=mHy=Hm
235 csbeq1 y=my/xB=m/xB
236 234 235 oveq12d y=mHyy/xB=Hmm/xB
237 eqid yVHyy/xB=yVHyy/xB
238 ovex Hyy/xBV
239 236 237 238 fvmpt3i mVyVHyy/xBm=Hmm/xB
240 239 elv yVHyy/xBm=Hmm/xB
241 144 217 syldan φX+1YmX+1Ym/xB
242 145 241 resubcld φX+1YmX+1YHmm/xB
243 240 242 eqeltrid φX+1YmX+1YyVHyy/xBm
244 198 simprd φX+1YmX+1Y1Hmm/xBHm+1m+1/xB
245 ovex m+1V
246 fveq2 y=m+1Hy=Hm+1
247 csbeq1 y=m+1y/xB=m+1/xB
248 246 247 oveq12d y=m+1Hyy/xB=Hm+1m+1/xB
249 248 237 238 fvmpt3i m+1VyVHyy/xBm+1=Hm+1m+1/xB
250 245 249 ax-mp yVHyy/xBm+1=Hm+1m+1/xB
251 244 240 250 3brtr4g φX+1YmX+1Y1yVHyy/xBmyVHyy/xBm+1
252 129 243 251 monoord φX+1YyVHyy/xBX+1yVHyy/xBY
253 ovex X+1V
254 fveq2 y=X+1Hy=HX+1
255 csbeq1 y=X+1y/xB=X+1/xB
256 254 255 oveq12d y=X+1Hyy/xB=HX+1X+1/xB
257 256 237 238 fvmpt3i X+1VyVHyy/xBX+1=HX+1X+1/xB
258 253 257 ax-mp yVHyy/xBX+1=HX+1X+1/xB
259 fvex YV
260 fveq2 y=YHy=HY
261 csbeq1 y=Yy/xB=Y/xB
262 260 261 oveq12d y=YHyy/xB=HYY/xB
263 262 237 238 fvmpt3i YVyVHyy/xBY=HYY/xB
264 259 263 ax-mp yVHyy/xBY=HYY/xB
265 252 258 264 3brtr3g φX+1YHX+1X+1/xBHYY/xB
266 220 232 224 233 265 letrd φX+1YHXX/xBHYY/xB
267 119 simprd φX+1YHYY/xBHYY/xB
268 220 224 228 266 267 letrd φX+1YHXX/xBHYY/xB
269 207 268 jca φX+1YHYHXHXX/xBHYY/xB
270 22 26 43 269 lecasei φHYHXHXX/xBHYY/xB