Metamath Proof Explorer


Theorem dvfsumlem2

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses dvfsum.s S = T +∞
dvfsum.z Z = M
dvfsum.m φ M
dvfsum.d φ D
dvfsum.md φ M D + 1
dvfsum.t φ T
dvfsum.a φ x S A
dvfsum.b1 φ x S B V
dvfsum.b2 φ x Z B
dvfsum.b3 φ dx S A d x = x S B
dvfsum.c x = k B = C
dvfsum.u φ U *
dvfsum.l φ x S k S D x x k k U C B
dvfsum.h H = x S x x B + k = M x C - A
dvfsumlem1.1 φ X S
dvfsumlem1.2 φ Y S
dvfsumlem1.3 φ D X
dvfsumlem1.4 φ X Y
dvfsumlem1.5 φ Y U
dvfsumlem1.6 φ Y X + 1
Assertion dvfsumlem2 φ H Y H X H X X / x B H Y Y / x B

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 φ M D + 1
6 dvfsum.t φ T
7 dvfsum.a φ x S A
8 dvfsum.b1 φ x S B V
9 dvfsum.b2 φ x Z B
10 dvfsum.b3 φ dx S A d x = x S B
11 dvfsum.c x = k B = C
12 dvfsum.u φ U *
13 dvfsum.l φ x S k S D x x k k U C B
14 dvfsum.h H = x S x x B + k = M x C - A
15 dvfsumlem1.1 φ X S
16 dvfsumlem1.2 φ Y S
17 dvfsumlem1.3 φ D X
18 dvfsumlem1.4 φ X Y
19 dvfsumlem1.5 φ Y U
20 dvfsumlem1.6 φ Y X + 1
21 ioossre T +∞
22 1 21 eqsstri S
23 22 16 sselid φ Y
24 15 1 eleqtrdi φ X T +∞
25 6 rexrd φ T *
26 elioopnf T * X T +∞ X T < X
27 25 26 syl φ X T +∞ X T < X
28 24 27 mpbid φ X T < X
29 28 simpld φ X
30 reflcl X X
31 29 30 syl φ X
32 23 31 resubcld φ Y X
33 csbeq1 y = Y y / x B = Y / x B
34 33 eleq1d y = Y y / x B Y / x B
35 22 a1i φ S
36 35 7 8 10 dvmptrecl φ x S B
37 36 fmpttd φ x S B : S
38 nfcv _ y B
39 nfcsb1v _ x y / x B
40 csbeq1a x = y B = y / x B
41 38 39 40 cbvmpt x S B = y S y / x B
42 41 fmpt y S y / x B x S B : S
43 37 42 sylibr φ y S y / x B
44 34 43 16 rspcdva φ Y / x B
45 32 44 remulcld φ Y X Y / x B
46 csbeq1 y = Y y / x A = Y / x A
47 46 eleq1d y = Y y / x A Y / x A
48 7 fmpttd φ x S A : S
49 nfcv _ y A
50 nfcsb1v _ x y / x A
51 csbeq1a x = y A = y / x A
52 49 50 51 cbvmpt x S A = y S y / x A
53 52 fmpt y S y / x A x S A : S
54 48 53 sylibr φ y S y / x A
55 47 54 16 rspcdva φ Y / x A
56 45 55 resubcld φ Y X Y / x B Y / x A
57 29 31 resubcld φ X X
58 csbeq1 y = X y / x B = X / x B
59 58 eleq1d y = X y / x B X / x B
60 59 43 15 rspcdva φ X / x B
61 57 60 remulcld φ X X X / x B
62 csbeq1 y = X y / x A = X / x A
63 62 eleq1d y = X y / x A X / x A
64 63 54 15 rspcdva φ X / x A
65 61 64 resubcld φ X X X / x B X / x A
66 fzfid φ M X Fin
67 9 ralrimiva φ x Z B
68 elfzuz k M X k M
69 68 2 eleqtrrdi k M X k Z
70 11 eleq1d x = k B C
71 70 rspccva x Z B k Z C
72 67 69 71 syl2an φ k M X C
73 66 72 fsumrecl φ k = M X C
74 57 44 remulcld φ X X Y / x B
75 74 64 resubcld φ X X Y / x B X / x A
76 23 29 resubcld φ Y X
77 44 76 remulcld φ Y / x B Y X
78 44 recnd φ Y / x B
79 23 recnd φ Y
80 29 recnd φ X
81 78 79 80 subdid φ Y / x B Y X = Y / x B Y Y / x B X
82 eqid TopOpen fld = TopOpen fld
83 82 mpomulcn u , v u v TopOpen fld × t TopOpen fld Cn TopOpen fld
84 csbeq1 z = Y z / x B = Y / x B
85 84 eleq1d z = Y z / x B Y / x B
86 nfcv _ z B
87 nfcsb1v _ x z / x B
88 csbeq1a x = z B = z / x B
89 86 87 88 cbvmpt x S B = z S z / x B
90 89 fmpt z S z / x B x S B : S
91 37 90 sylibr φ z S z / x B
92 85 91 16 rspcdva φ Y / x B
93 pnfxr +∞ *
94 93 a1i φ +∞ *
95 28 simprd φ T < X
96 23 ltpnfd φ Y < +∞
97 iccssioo T * +∞ * T < X Y < +∞ X Y T +∞
98 25 94 95 96 97 syl22anc φ X Y T +∞
99 98 21 sstrdi φ X Y
100 ax-resscn
101 99 100 sstrdi φ X Y
102 100 a1i φ
103 cncfmptc Y / x B X Y y X Y Y / x B : X Y cn
104 92 101 102 103 syl3anc φ y X Y Y / x B : X Y cn
105 cncfmptid X Y y X Y y : X Y cn
106 99 100 105 sylancl φ y X Y y : X Y cn
107 remulcl Y / x B y Y / x B y
108 simpl Y / x B y Y / x B
109 108 recnd Y / x B y Y / x B
110 simpr Y / x B y y
111 110 recnd Y / x B y y
112 109 111 jca Y / x B y Y / x B y
113 ovmpot Y / x B y Y / x B u , v u v y = Y / x B y
114 113 eqcomd Y / x B y Y / x B y = Y / x B u , v u v y
115 112 114 syl Y / x B y Y / x B y = Y / x B u , v u v y
116 115 eleq1d Y / x B y Y / x B y Y / x B u , v u v y
117 116 biimpd Y / x B y Y / x B y Y / x B u , v u v y
118 107 117 mpd Y / x B y Y / x B u , v u v y
119 82 83 104 106 100 118 cncfmpt2ss φ y X Y Y / x B u , v u v y : X Y cn
120 df-mpt y X Y Y / x B u , v u v y = y w | y X Y w = Y / x B u , v u v y
121 120 eleq1i y X Y Y / x B u , v u v y : X Y cn y w | y X Y w = Y / x B u , v u v y : X Y cn
122 121 biimpi y X Y Y / x B u , v u v y : X Y cn y w | y X Y w = Y / x B u , v u v y : X Y cn
123 119 122 syl φ y w | y X Y w = Y / x B u , v u v y : X Y cn
124 idd φ y X Y y X Y
125 124 a1dd φ y X Y w = Y / x B u , v u v y y X Y
126 125 impd φ y X Y w = Y / x B u , v u v y y X Y
127 csbeq1 m = Y m / x B = Y / x B
128 127 eleq1d m = Y m / x B Y / x B
129 nfcv _ m B
130 nfcsb1v _ x m / x B
131 csbeq1a x = m B = m / x B
132 129 130 131 cbvmpt x S B = m S m / x B
133 132 fmpt m S m / x B x S B : S
134 37 133 sylibr φ m S m / x B
135 128 134 16 rspcdva φ Y / x B
136 135 recnd φ Y / x B
137 136 adantr φ y X Y Y / x B
138 elicc2 X Y y X Y y X y y Y
139 29 23 138 syl2anc φ y X Y y X y y Y
140 139 biimpa φ y X Y y X y y Y
141 140 simp1d φ y X Y y
142 141 recnd φ y X Y y
143 137 142 jca φ y X Y Y / x B y
144 143 113 syl φ y X Y Y / x B u , v u v y = Y / x B y
145 144 eqeq2d φ y X Y w = Y / x B u , v u v y w = Y / x B y
146 145 biimpd φ y X Y w = Y / x B u , v u v y w = Y / x B y
147 146 ex φ y X Y w = Y / x B u , v u v y w = Y / x B y
148 147 impd φ y X Y w = Y / x B u , v u v y w = Y / x B y
149 126 148 jcad φ y X Y w = Y / x B u , v u v y y X Y w = Y / x B y
150 124 a1dd φ y X Y w = Y / x B y y X Y
151 150 impd φ y X Y w = Y / x B y y X Y
152 csbeq1 k = Y k / x B = Y / x B
153 152 eleq1d k = Y k / x B Y / x B
154 nfcv _ k B
155 nfcsb1v _ x k / x B
156 csbeq1a x = k B = k / x B
157 154 155 156 cbvmpt x S B = k S k / x B
158 157 fmpt k S k / x B x S B : S
159 37 158 sylibr φ k S k / x B
160 153 159 16 rspcdva φ Y / x B
161 160 recnd φ Y / x B
162 161 adantr φ y X Y Y / x B
163 162 142 jca φ y X Y Y / x B y
164 163 114 syl φ y X Y Y / x B y = Y / x B u , v u v y
165 164 eqeq2d φ y X Y w = Y / x B y w = Y / x B u , v u v y
166 165 biimpd φ y X Y w = Y / x B y w = Y / x B u , v u v y
167 166 ex φ y X Y w = Y / x B y w = Y / x B u , v u v y
168 167 impd φ y X Y w = Y / x B y w = Y / x B u , v u v y
169 151 168 jcad φ y X Y w = Y / x B y y X Y w = Y / x B u , v u v y
170 149 169 impbid φ y X Y w = Y / x B u , v u v y y X Y w = Y / x B y
171 170 opabbidv φ y w | y X Y w = Y / x B u , v u v y = y w | y X Y w = Y / x B y
172 df-mpt y X Y Y / x B y = y w | y X Y w = Y / x B y
173 172 eqcomi y w | y X Y w = Y / x B y = y X Y Y / x B y
174 173 eqeq2i y w | y X Y w = Y / x B u , v u v y = y w | y X Y w = Y / x B y y w | y X Y w = Y / x B u , v u v y = y X Y Y / x B y
175 174 biimpi y w | y X Y w = Y / x B u , v u v y = y w | y X Y w = Y / x B y y w | y X Y w = Y / x B u , v u v y = y X Y Y / x B y
176 171 175 syl φ y w | y X Y w = Y / x B u , v u v y = y X Y Y / x B y
177 176 eleq1d φ y w | y X Y w = Y / x B u , v u v y : X Y cn y X Y Y / x B y : X Y cn
178 177 biimpd φ y w | y X Y w = Y / x B u , v u v y : X Y cn y X Y Y / x B y : X Y cn
179 123 178 mpd φ y X Y Y / x B y : X Y cn
180 reelprrecn
181 180 a1i φ
182 ioossicc X Y X Y
183 182 99 sstrid φ X Y
184 183 sselda φ y X Y y
185 184 recnd φ y X Y y
186 1cnd φ y X Y 1
187 simpr φ y y
188 187 recnd φ y y
189 1cnd φ y 1
190 181 dvmptid φ dy y d y = y 1
191 82 tgioo2 topGen ran . = TopOpen fld 𝑡
192 iooretop X Y topGen ran .
193 192 a1i φ X Y topGen ran .
194 181 188 189 190 183 191 82 193 dvmptres φ dy X Y y d y = y X Y 1
195 181 185 186 194 78 dvmptcmul φ dy X Y Y / x B y d y = y X Y Y / x B 1
196 78 mulridd φ Y / x B 1 = Y / x B
197 196 mpteq2dv φ y X Y Y / x B 1 = y X Y Y / x B
198 195 197 eqtrd φ dy X Y Y / x B y d y = y X Y Y / x B
199 98 1 sseqtrrdi φ X Y S
200 199 resmptd φ y S y / x A X Y = y X Y y / x A
201 7 recnd φ x S A
202 201 fmpttd φ x S A : S
203 10 dmeqd φ dom dx S A d x = dom x S B
204 8 ralrimiva φ x S B V
205 dmmptg x S B V dom x S B = S
206 204 205 syl φ dom x S B = S
207 203 206 eqtrd φ dom dx S A d x = S
208 dvcn x S A : S S dom dx S A d x = S x S A : S cn
209 102 202 35 207 208 syl31anc φ x S A : S cn
210 cncfcdm x S A : S cn x S A : S cn x S A : S
211 100 209 210 sylancr φ x S A : S cn x S A : S
212 48 211 mpbird φ x S A : S cn
213 52 212 eqeltrrid φ y S y / x A : S cn
214 rescncf X Y S y S y / x A : S cn y S y / x A X Y : X Y cn
215 199 213 214 sylc φ y S y / x A X Y : X Y cn
216 200 215 eqeltrrd φ y X Y y / x A : X Y cn
217 54 r19.21bi φ y S y / x A
218 217 recnd φ y S y / x A
219 43 r19.21bi φ y S y / x B
220 52 oveq2i dx S A d x = dy S y / x A d y
221 10 220 41 3eqtr3g φ dy S y / x A d y = y S y / x B
222 182 199 sstrid φ X Y S
223 181 218 219 221 222 191 82 193 dvmptres φ dy X Y y / x A d y = y X Y y / x B
224 182 sseli y X Y y X Y
225 simpl φ y X Y φ
226 199 sselda φ y X Y y S
227 16 adantr φ y X Y Y S
228 4 adantr φ y X Y D
229 29 adantr φ y X Y X
230 17 adantr φ y X Y D X
231 140 simp2d φ y X Y X y
232 228 229 141 230 231 letrd φ y X Y D y
233 140 simp3d φ y X Y y Y
234 19 adantr φ y X Y Y U
235 simp2r φ y S Y S D y y Y Y U Y S
236 eleq1 k = Y k S Y S
237 236 anbi2d k = Y y S k S y S Y S
238 breq2 k = Y y k y Y
239 breq1 k = Y k U Y U
240 238 239 3anbi23d k = Y D y y k k U D y y Y Y U
241 237 240 3anbi23d k = Y φ y S k S D y y k k U φ y S Y S D y y Y Y U
242 vex k V
243 242 11 csbie k / x B = C
244 243 152 eqtr3id k = Y C = Y / x B
245 244 breq1d k = Y C y / x B Y / x B y / x B
246 241 245 imbi12d k = Y φ y S k S D y y k k U C y / x B φ y S Y S D y y Y Y U Y / x B y / x B
247 nfv x φ y S k S D y y k k U
248 nfcv _ x C
249 nfcv _ x
250 248 249 39 nfbr x C y / x B
251 247 250 nfim x φ y S k S D y y k k U C y / x B
252 eleq1 x = y x S y S
253 252 anbi1d x = y x S k S y S k S
254 breq2 x = y D x D y
255 breq1 x = y x k y k
256 254 255 3anbi12d x = y D x x k k U D y y k k U
257 253 256 3anbi23d x = y φ x S k S D x x k k U φ y S k S D y y k k U
258 40 breq2d x = y C B C y / x B
259 257 258 imbi12d x = y φ x S k S D x x k k U C B φ y S k S D y y k k U C y / x B
260 251 259 13 chvarfv φ y S k S D y y k k U C y / x B
261 246 260 vtoclg Y S φ y S Y S D y y Y Y U Y / x B y / x B
262 235 261 mpcom φ y S Y S D y y Y Y U Y / x B y / x B
263 225 226 227 232 233 234 262 syl123anc φ y X Y Y / x B y / x B
264 224 263 sylan2 φ y X Y Y / x B y / x B
265 29 rexrd φ X *
266 23 rexrd φ Y *
267 lbicc2 X * Y * X Y X X Y
268 265 266 18 267 syl3anc φ X X Y
269 ubicc2 X * Y * X Y Y X Y
270 265 266 18 269 syl3anc φ Y X Y
271 oveq2 y = X Y / x B y = Y / x B X
272 oveq2 y = Y Y / x B y = Y / x B Y
273 29 23 179 198 216 223 264 268 270 18 271 62 272 46 dvle φ Y / x B Y Y / x B X Y / x A X / x A
274 81 273 eqbrtrd φ Y / x B Y X Y / x A X / x A
275 77 55 64 274 lesubd φ X / x A Y / x A Y / x B Y X
276 74 recnd φ X X Y / x B
277 45 recnd φ Y X Y / x B
278 55 recnd φ Y / x A
279 276 277 278 subsubd φ X X Y / x B Y X Y / x B Y / x A = X X Y / x B - Y X Y / x B + Y / x A
280 277 276 negsubdi2d φ Y X Y / x B X X Y / x B = X X Y / x B Y X Y / x B
281 31 recnd φ X
282 79 80 281 nnncan2d φ Y - X - X X = Y X
283 282 oveq1d φ Y - X - X X Y / x B = Y X Y / x B
284 32 recnd φ Y X
285 57 recnd φ X X
286 284 285 78 subdird φ Y - X - X X Y / x B = Y X Y / x B X X Y / x B
287 76 recnd φ Y X
288 287 78 mulcomd φ Y X Y / x B = Y / x B Y X
289 283 286 288 3eqtr3d φ Y X Y / x B X X Y / x B = Y / x B Y X
290 289 negeqd φ Y X Y / x B X X Y / x B = Y / x B Y X
291 280 290 eqtr3d φ X X Y / x B Y X Y / x B = Y / x B Y X
292 291 oveq1d φ X X Y / x B - Y X Y / x B + Y / x A = - Y / x B Y X + Y / x A
293 77 recnd φ Y / x B Y X
294 293 278 negsubdid φ Y / x B Y X Y / x A = - Y / x B Y X + Y / x A
295 292 294 eqtr4d φ X X Y / x B - Y X Y / x B + Y / x A = Y / x B Y X Y / x A
296 293 278 negsubdi2d φ Y / x B Y X Y / x A = Y / x A Y / x B Y X
297 279 295 296 3eqtrd φ X X Y / x B Y X Y / x B Y / x A = Y / x A Y / x B Y X
298 275 297 breqtrrd φ X / x A X X Y / x B Y X Y / x B Y / x A
299 64 74 56 298 lesubd φ Y X Y / x B Y / x A X X Y / x B X / x A
300 flle X X X
301 29 300 syl φ X X
302 29 31 subge0d φ 0 X X X X
303 301 302 mpbird φ 0 X X
304 58 breq2d y = X Y / x B y / x B Y / x B X / x B
305 263 ralrimiva φ y X Y Y / x B y / x B
306 304 305 268 rspcdva φ Y / x B X / x B
307 44 60 57 303 306 lemul2ad φ X X Y / x B X X X / x B
308 74 61 64 307 lesub1dd φ X X Y / x B X / x A X X X / x B X / x A
309 56 75 65 299 308 letrd φ Y X Y / x B Y / x A X X X / x B X / x A
310 56 65 73 309 leadd1dd φ Y X Y / x B - Y / x A + k = M X C X X X / x B - X / x A + k = M X C
311 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dvfsumlem1 φ H Y = Y X Y / x B - Y / x A + k = M X C
312 29 leidd φ X X
313 265 266 12 18 19 xrletrd φ X U
314 fllep1 X X X + 1
315 29 314 syl φ X X + 1
316 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 312 313 315 dvfsumlem1 φ H X = X X X / x B - X / x A + k = M X C
317 310 311 316 3brtr4d φ H Y H X
318 65 60 resubcld φ X X X / x B - X / x A - X / x B
319 56 44 resubcld φ Y X Y / x B - Y / x A - Y / x B
320 peano2rem X X X - X - 1
321 57 320 syl φ X - X - 1
322 321 60 remulcld φ X - X - 1 X / x B
323 322 64 resubcld φ X - X - 1 X / x B X / x A
324 peano2rem Y X Y - X - 1
325 32 324 syl φ Y - X - 1
326 325 60 remulcld φ Y - X - 1 X / x B
327 326 55 resubcld φ Y - X - 1 X / x B Y / x A
328 325 44 remulcld φ Y - X - 1 Y / x B
329 328 55 resubcld φ Y - X - 1 Y / x B Y / x A
330 322 recnd φ X - X - 1 X / x B
331 326 recnd φ Y - X - 1 X / x B
332 330 331 subcld φ X - X - 1 X / x B Y - X - 1 X / x B
333 332 278 addcomd φ X - X - 1 X / x B - Y - X - 1 X / x B + Y / x A = Y / x A + X - X - 1 X / x B - Y - X - 1 X / x B
334 330 331 278 subsubd φ X - X - 1 X / x B Y - X - 1 X / x B Y / x A = X - X - 1 X / x B - Y - X - 1 X / x B + Y / x A
335 278 331 330 subsub2d φ Y / x A Y - X - 1 X / x B X - X - 1 X / x B = Y / x A + X - X - 1 X / x B - Y - X - 1 X / x B
336 333 334 335 3eqtr4d φ X - X - 1 X / x B Y - X - 1 X / x B Y / x A = Y / x A Y - X - 1 X / x B X - X - 1 X / x B
337 1cnd φ 1
338 284 285 337 nnncan2d φ Y X - 1 - X - X - 1 = Y - X - X X
339 338 282 eqtrd φ Y X - 1 - X - X - 1 = Y X
340 339 oveq1d φ Y X - 1 - X - X - 1 X / x B = Y X X / x B
341 325 recnd φ Y - X - 1
342 321 recnd φ X - X - 1
343 60 recnd φ X / x B
344 341 342 343 subdird φ Y X - 1 - X - X - 1 X / x B = Y - X - 1 X / x B X - X - 1 X / x B
345 287 343 mulcomd φ Y X X / x B = X / x B Y X
346 340 344 345 3eqtr3d φ Y - X - 1 X / x B X - X - 1 X / x B = X / x B Y X
347 346 oveq2d φ Y / x A Y - X - 1 X / x B X - X - 1 X / x B = Y / x A X / x B Y X
348 336 347 eqtrd φ X - X - 1 X / x B Y - X - 1 X / x B Y / x A = Y / x A X / x B Y X
349 60 76 remulcld φ X / x B Y X
350 cncfmptc X / x B X Y y X Y X / x B : X Y cn
351 60 101 102 350 syl3anc φ y X Y X / x B : X Y cn
352 remulcl X / x B y X / x B y
353 simpl X / x B y X / x B
354 353 recnd X / x B y X / x B
355 simpr X / x B y y
356 355 recnd X / x B y y
357 354 356 jca X / x B y X / x B y
358 ovmpot X / x B y X / x B u , v u v y = X / x B y
359 358 eqcomd X / x B y X / x B y = X / x B u , v u v y
360 357 359 syl X / x B y X / x B y = X / x B u , v u v y
361 360 eleq1d X / x B y X / x B y X / x B u , v u v y
362 361 biimpd X / x B y X / x B y X / x B u , v u v y
363 352 362 mpd X / x B y X / x B u , v u v y
364 82 83 351 106 100 363 cncfmpt2ss φ y X Y X / x B u , v u v y : X Y cn
365 df-mpt y X Y X / x B u , v u v y = y w | y X Y w = X / x B u , v u v y
366 365 eleq1i y X Y X / x B u , v u v y : X Y cn y w | y X Y w = X / x B u , v u v y : X Y cn
367 366 biimpi y X Y X / x B u , v u v y : X Y cn y w | y X Y w = X / x B u , v u v y : X Y cn
368 364 367 syl φ y w | y X Y w = X / x B u , v u v y : X Y cn
369 124 a1dd φ y X Y w = X / x B u , v u v y y X Y
370 369 impd φ y X Y w = X / x B u , v u v y y X Y
371 343 adantr φ y X Y X / x B
372 371 142 jca φ y X Y X / x B y
373 372 358 syl φ y X Y X / x B u , v u v y = X / x B y
374 373 eqeq2d φ y X Y w = X / x B u , v u v y w = X / x B y
375 374 biimpd φ y X Y w = X / x B u , v u v y w = X / x B y
376 375 ex φ y X Y w = X / x B u , v u v y w = X / x B y
377 376 impd φ y X Y w = X / x B u , v u v y w = X / x B y
378 370 377 jcad φ y X Y w = X / x B u , v u v y y X Y w = X / x B y
379 124 a1dd φ y X Y w = X / x B y y X Y
380 379 impd φ y X Y w = X / x B y y X Y
381 372 359 syl φ y X Y X / x B y = X / x B u , v u v y
382 381 eqeq2d φ y X Y w = X / x B y w = X / x B u , v u v y
383 382 biimpd φ y X Y w = X / x B y w = X / x B u , v u v y
384 383 ex φ y X Y w = X / x B y w = X / x B u , v u v y
385 384 impd φ y X Y w = X / x B y w = X / x B u , v u v y
386 380 385 jcad φ y X Y w = X / x B y y X Y w = X / x B u , v u v y
387 378 386 impbid φ y X Y w = X / x B u , v u v y y X Y w = X / x B y
388 387 opabbidv φ y w | y X Y w = X / x B u , v u v y = y w | y X Y w = X / x B y
389 df-mpt y X Y X / x B y = y w | y X Y w = X / x B y
390 389 eqcomi y w | y X Y w = X / x B y = y X Y X / x B y
391 390 eqeq2i y w | y X Y w = X / x B u , v u v y = y w | y X Y w = X / x B y y w | y X Y w = X / x B u , v u v y = y X Y X / x B y
392 391 biimpi y w | y X Y w = X / x B u , v u v y = y w | y X Y w = X / x B y y w | y X Y w = X / x B u , v u v y = y X Y X / x B y
393 388 392 syl φ y w | y X Y w = X / x B u , v u v y = y X Y X / x B y
394 393 eleq1d φ y w | y X Y w = X / x B u , v u v y : X Y cn y X Y X / x B y : X Y cn
395 394 biimpd φ y w | y X Y w = X / x B u , v u v y : X Y cn y X Y X / x B y : X Y cn
396 368 395 mpd φ y X Y X / x B y : X Y cn
397 181 185 186 194 343 dvmptcmul φ dy X Y X / x B y d y = y X Y X / x B 1
398 343 mulridd φ X / x B 1 = X / x B
399 398 mpteq2dv φ y X Y X / x B 1 = y X Y X / x B
400 397 399 eqtrd φ dy X Y X / x B y d y = y X Y X / x B
401 15 adantr φ y X Y X S
402 141 rexrd φ y X Y y *
403 266 adantr φ y X Y Y *
404 12 adantr φ y X Y U *
405 402 403 404 233 234 xrletrd φ y X Y y U
406 vex y V
407 eleq1 k = y k S y S
408 407 anbi2d k = y X S k S X S y S
409 breq2 k = y X k X y
410 breq1 k = y k U y U
411 409 410 3anbi23d k = y D X X k k U D X X y y U
412 408 411 3anbi23d k = y φ X S k S D X X k k U φ X S y S D X X y y U
413 csbeq1 k = y k / x B = y / x B
414 243 413 eqtr3id k = y C = y / x B
415 414 breq1d k = y C X / x B y / x B X / x B
416 412 415 imbi12d k = y φ X S k S D X X k k U C X / x B φ X S y S D X X y y U y / x B X / x B
417 simp2l φ X S k S D X X k k U X S
418 nfv x φ X S k S D X X k k U
419 nfcsb1v _ x X / x B
420 248 249 419 nfbr x C X / x B
421 418 420 nfim x φ X S k S D X X k k U C X / x B
422 eleq1 x = X x S X S
423 422 anbi1d x = X x S k S X S k S
424 breq2 x = X D x D X
425 breq1 x = X x k X k
426 424 425 3anbi12d x = X D x x k k U D X X k k U
427 423 426 3anbi23d x = X φ x S k S D x x k k U φ X S k S D X X k k U
428 csbeq1a x = X B = X / x B
429 428 breq2d x = X C B C X / x B
430 427 429 imbi12d x = X φ x S k S D x x k k U C B φ X S k S D X X k k U C X / x B
431 421 430 13 vtoclg1f X S φ X S k S D X X k k U C X / x B
432 417 431 mpcom φ X S k S D X X k k U C X / x B
433 406 416 432 vtocl φ X S y S D X X y y U y / x B X / x B
434 225 401 226 230 231 405 433 syl123anc φ y X Y y / x B X / x B
435 224 434 sylan2 φ y X Y y / x B X / x B
436 oveq2 y = X X / x B y = X / x B X
437 oveq2 y = Y X / x B y = X / x B Y
438 29 23 216 223 396 400 435 268 270 18 62 436 46 437 dvle φ Y / x A X / x A X / x B Y X / x B X
439 343 79 80 subdid φ X / x B Y X = X / x B Y X / x B X
440 438 439 breqtrrd φ Y / x A X / x A X / x B Y X
441 55 64 349 440 subled φ Y / x A X / x B Y X X / x A
442 348 441 eqbrtrd φ X - X - 1 X / x B Y - X - 1 X / x B Y / x A X / x A
443 322 327 64 442 subled φ X - X - 1 X / x B X / x A Y - X - 1 X / x B Y / x A
444 325 renegcld φ Y - X - 1
445 1red φ 1
446 23 31 445 lesubadd2d φ Y X 1 Y X + 1
447 20 446 mpbird φ Y X 1
448 32 445 suble0d φ Y - X - 1 0 Y X 1
449 447 448 mpbird φ Y - X - 1 0
450 325 le0neg1d φ Y - X - 1 0 0 Y - X - 1
451 449 450 mpbid φ 0 Y - X - 1
452 44 60 444 451 306 lemul2ad φ Y - X - 1 Y / x B Y - X - 1 X / x B
453 341 78 mulneg1d φ Y - X - 1 Y / x B = Y - X - 1 Y / x B
454 341 343 mulneg1d φ Y - X - 1 X / x B = Y - X - 1 X / x B
455 452 453 454 3brtr3d φ Y - X - 1 Y / x B Y - X - 1 X / x B
456 326 328 lenegd φ Y - X - 1 X / x B Y - X - 1 Y / x B Y - X - 1 Y / x B Y - X - 1 X / x B
457 455 456 mpbird φ Y - X - 1 X / x B Y - X - 1 Y / x B
458 326 328 55 457 lesub1dd φ Y - X - 1 X / x B Y / x A Y - X - 1 Y / x B Y / x A
459 323 327 329 443 458 letrd φ X - X - 1 X / x B X / x A Y - X - 1 Y / x B Y / x A
460 285 337 343 subdird φ X - X - 1 X / x B = X X X / x B 1 X / x B
461 343 mullidd φ 1 X / x B = X / x B
462 461 oveq2d φ X X X / x B 1 X / x B = X X X / x B X / x B
463 460 462 eqtrd φ X - X - 1 X / x B = X X X / x B X / x B
464 463 oveq1d φ X - X - 1 X / x B X / x A = X X X / x B - X / x B - X / x A
465 284 337 78 subdird φ Y - X - 1 Y / x B = Y X Y / x B 1 Y / x B
466 78 mullidd φ 1 Y / x B = Y / x B
467 466 oveq2d φ Y X Y / x B 1 Y / x B = Y X Y / x B Y / x B
468 465 467 eqtrd φ Y - X - 1 Y / x B = Y X Y / x B Y / x B
469 468 oveq1d φ Y - X - 1 Y / x B Y / x A = Y X Y / x B - Y / x B - Y / x A
470 459 464 469 3brtr3d φ X X X / x B - X / x B - X / x A Y X Y / x B - Y / x B - Y / x A
471 61 recnd φ X X X / x B
472 64 recnd φ X / x A
473 471 472 343 sub32d φ X X X / x B - X / x A - X / x B = X X X / x B - X / x B - X / x A
474 277 278 78 sub32d φ Y X Y / x B - Y / x A - Y / x B = Y X Y / x B - Y / x B - Y / x A
475 470 473 474 3brtr4d φ X X X / x B - X / x A - X / x B Y X Y / x B - Y / x A - Y / x B
476 318 319 73 475 leadd1dd φ X X X / x B X / x A - X / x B + k = M X C Y X Y / x B Y / x A - Y / x B + k = M X C
477 65 recnd φ X X X / x B X / x A
478 73 recnd φ k = M X C
479 477 478 343 addsubd φ X X X / x B X / x A + k = M X C - X / x B = X X X / x B X / x A - X / x B + k = M X C
480 56 recnd φ Y X Y / x B Y / x A
481 480 478 78 addsubd φ Y X Y / x B Y / x A + k = M X C - Y / x B = Y X Y / x B Y / x A - Y / x B + k = M X C
482 476 479 481 3brtr4d φ X X X / x B X / x A + k = M X C - X / x B Y X Y / x B Y / x A + k = M X C - Y / x B
483 316 oveq1d φ H X X / x B = X X X / x B X / x A + k = M X C - X / x B
484 311 oveq1d φ H Y Y / x B = Y X Y / x B Y / x A + k = M X C - Y / x B
485 482 483 484 3brtr4d φ H X X / x B H Y Y / x B
486 317 485 jca φ H Y H X H X X / x B H Y Y / x B