Metamath Proof Explorer


Theorem uniioombllem3

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
uniioombl.a A = ran . F
uniioombl.e φ vol * E
uniioombl.c φ C +
uniioombl.g φ G : 2
uniioombl.s φ E ran . G
uniioombl.t T = seq 1 + abs G
uniioombl.v φ sup ran T * < vol * E + C
uniioombl.m φ M
uniioombl.m2 φ T M sup ran T * < < C
uniioombl.k K = . G 1 M
Assertion uniioombllem3 φ vol * E A + vol * E A < vol * K A + vol * K A + C + C

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 uniioombl.a A = ran . F
5 uniioombl.e φ vol * E
6 uniioombl.c φ C +
7 uniioombl.g φ G : 2
8 uniioombl.s φ E ran . G
9 uniioombl.t T = seq 1 + abs G
10 uniioombl.v φ sup ran T * < vol * E + C
11 uniioombl.m φ M
12 uniioombl.m2 φ T M sup ran T * < < C
13 uniioombl.k K = . G 1 M
14 inss1 E A E
15 14 a1i φ E A E
16 7 uniiccdif φ ran . G ran . G vol * ran . G ran . G = 0
17 16 simpld φ ran . G ran . G
18 ovolficcss G : 2 ran . G
19 7 18 syl φ ran . G
20 17 19 sstrd φ ran . G
21 8 20 sstrd φ E
22 ovolsscl E A E E vol * E vol * E A
23 15 21 5 22 syl3anc φ vol * E A
24 difssd φ E A E
25 ovolsscl E A E E vol * E vol * E A
26 24 21 5 25 syl3anc φ vol * E A
27 inss1 K A K
28 27 a1i φ K A K
29 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3a φ K = j = 1 M . G j vol * K
30 29 simpld φ K = j = 1 M . G j
31 inss2 2 2
32 elfznn j 1 M j
33 ffvelrn G : 2 j G j 2
34 7 32 33 syl2an φ j 1 M G j 2
35 31 34 sseldi φ j 1 M G j 2
36 1st2nd2 G j 2 G j = 1 st G j 2 nd G j
37 35 36 syl φ j 1 M G j = 1 st G j 2 nd G j
38 37 fveq2d φ j 1 M . G j = . 1 st G j 2 nd G j
39 df-ov 1 st G j 2 nd G j = . 1 st G j 2 nd G j
40 38 39 syl6eqr φ j 1 M . G j = 1 st G j 2 nd G j
41 ioossre 1 st G j 2 nd G j
42 40 41 eqsstrdi φ j 1 M . G j
43 42 ralrimiva φ j 1 M . G j
44 iunss j = 1 M . G j j 1 M . G j
45 43 44 sylibr φ j = 1 M . G j
46 30 45 eqsstrd φ K
47 29 simprd φ vol * K
48 ovolsscl K A K K vol * K vol * K A
49 28 46 47 48 syl3anc φ vol * K A
50 6 rpred φ C
51 49 50 readdcld φ vol * K A + C
52 difssd φ K A K
53 ovolsscl K A K K vol * K vol * K A
54 52 46 47 53 syl3anc φ vol * K A
55 54 50 readdcld φ vol * K A + C
56 ssun2 . G M + 1 K . G M + 1
57 ioof . : * × * 𝒫
58 rexpssxrxp 2 * × *
59 31 58 sstri 2 * × *
60 fss G : 2 2 * × * G : * × *
61 7 59 60 sylancl φ G : * × *
62 fco . : * × * 𝒫 G : * × * . G : 𝒫
63 57 61 62 sylancr φ . G : 𝒫
64 63 ffnd φ . G Fn
65 fnima . G Fn . G = ran . G
66 64 65 syl φ . G = ran . G
67 nnuz = 1
68 11 peano2nnd φ M + 1
69 68 67 eleqtrdi φ M + 1 1
70 uzsplit M + 1 1 1 = 1 M + 1 - 1 M + 1
71 69 70 syl φ 1 = 1 M + 1 - 1 M + 1
72 67 71 syl5eq φ = 1 M + 1 - 1 M + 1
73 11 nncnd φ M
74 ax-1cn 1
75 pncan M 1 M + 1 - 1 = M
76 73 74 75 sylancl φ M + 1 - 1 = M
77 76 oveq2d φ 1 M + 1 - 1 = 1 M
78 77 uneq1d φ 1 M + 1 - 1 M + 1 = 1 M M + 1
79 72 78 eqtrd φ = 1 M M + 1
80 79 imaeq2d φ . G = . G 1 M M + 1
81 66 80 eqtr3d φ ran . G = . G 1 M M + 1
82 imaundi . G 1 M M + 1 = . G 1 M . G M + 1
83 81 82 syl6eq φ ran . G = . G 1 M . G M + 1
84 83 unieqd φ ran . G = . G 1 M . G M + 1
85 uniun . G 1 M . G M + 1 = . G 1 M . G M + 1
86 84 85 syl6eq φ ran . G = . G 1 M . G M + 1
87 13 uneq1i K . G M + 1 = . G 1 M . G M + 1
88 86 87 syl6eqr φ ran . G = K . G M + 1
89 56 88 sseqtrrid φ . G M + 1 ran . G
90 1 2 3 4 5 6 7 8 9 10 uniioombllem1 φ sup ran T * <
91 ssid ran . G ran . G
92 9 ovollb G : 2 ran . G ran . G vol * ran . G sup ran T * <
93 7 91 92 sylancl φ vol * ran . G sup ran T * <
94 ovollecl ran . G sup ran T * < vol * ran . G sup ran T * < vol * ran . G
95 20 90 93 94 syl3anc φ vol * ran . G
96 ovolsscl . G M + 1 ran . G ran . G vol * ran . G vol * . G M + 1
97 89 20 95 96 syl3anc φ vol * . G M + 1
98 49 97 readdcld φ vol * K A + vol * . G M + 1
99 unss1 K A K K A . G M + 1 K . G M + 1
100 27 99 ax-mp K A . G M + 1 K . G M + 1
101 100 88 sseqtrrid φ K A . G M + 1 ran . G
102 ovolsscl K A . G M + 1 ran . G ran . G vol * ran . G vol * K A . G M + 1
103 101 20 95 102 syl3anc φ vol * K A . G M + 1
104 8 88 sseqtrd φ E K . G M + 1
105 104 ssrind φ E A K . G M + 1 A
106 indir K . G M + 1 A = K A . G M + 1 A
107 inss1 . G M + 1 A . G M + 1
108 unss2 . G M + 1 A . G M + 1 K A . G M + 1 A K A . G M + 1
109 107 108 ax-mp K A . G M + 1 A K A . G M + 1
110 106 109 eqsstri K . G M + 1 A K A . G M + 1
111 105 110 sstrdi φ E A K A . G M + 1
112 101 20 sstrd φ K A . G M + 1
113 ovolss E A K A . G M + 1 K A . G M + 1 vol * E A vol * K A . G M + 1
114 111 112 113 syl2anc φ vol * E A vol * K A . G M + 1
115 28 46 sstrd φ K A
116 89 20 sstrd φ . G M + 1
117 ovolun K A vol * K A . G M + 1 vol * . G M + 1 vol * K A . G M + 1 vol * K A + vol * . G M + 1
118 115 49 116 97 117 syl22anc φ vol * K A . G M + 1 vol * K A + vol * . G M + 1
119 23 103 98 114 118 letrd φ vol * E A vol * K A + vol * . G M + 1
120 rge0ssre 0 +∞
121 eqid abs G = abs G
122 121 9 ovolsf G : 2 T : 0 +∞
123 7 122 syl φ T : 0 +∞
124 123 11 ffvelrnd φ T M 0 +∞
125 120 124 sseldi φ T M
126 90 125 resubcld φ sup ran T * < T M
127 97 rexrd φ vol * . G M + 1 *
128 id z z
129 nnaddcl z M z + M
130 128 11 129 syl2anr φ z z + M
131 7 ffvelrnda φ z + M G z + M 2
132 130 131 syldan φ z G z + M 2
133 132 fmpttd φ z G z + M : 2
134 eqid abs z G z + M = abs z G z + M
135 eqid seq 1 + abs z G z + M = seq 1 + abs z G z + M
136 134 135 ovolsf z G z + M : 2 seq 1 + abs z G z + M : 0 +∞
137 133 136 syl φ seq 1 + abs z G z + M : 0 +∞
138 137 frnd φ ran seq 1 + abs z G z + M 0 +∞
139 icossxr 0 +∞ *
140 138 139 sstrdi φ ran seq 1 + abs z G z + M *
141 supxrcl ran seq 1 + abs z G z + M * sup ran seq 1 + abs z G z + M * < *
142 140 141 syl φ sup ran seq 1 + abs z G z + M * < *
143 126 rexrd φ sup ran T * < T M *
144 1zzd φ x M + 1 1
145 11 nnzd φ M
146 145 adantr φ x M + 1 M
147 addcom M 1 M + 1 = 1 + M
148 73 74 147 sylancl φ M + 1 = 1 + M
149 148 fveq2d φ M + 1 = 1 + M
150 149 eleq2d φ x M + 1 x 1 + M
151 150 biimpa φ x M + 1 x 1 + M
152 eluzsub 1 M x 1 + M x M 1
153 144 146 151 152 syl3anc φ x M + 1 x M 1
154 153 67 eleqtrrdi φ x M + 1 x M
155 eluzelz x M + 1 x
156 155 adantl φ x M + 1 x
157 156 zcnd φ x M + 1 x
158 73 adantr φ x M + 1 M
159 157 158 npcand φ x M + 1 x - M + M = x
160 159 eqcomd φ x M + 1 x = x - M + M
161 oveq1 z = x M z + M = x - M + M
162 161 rspceeqv x M x = x - M + M z x = z + M
163 154 160 162 syl2anc φ x M + 1 z x = z + M
164 eqid z z + M = z z + M
165 164 elrnmpt x V x ran z z + M z x = z + M
166 165 elv x ran z z + M z x = z + M
167 163 166 sylibr φ x M + 1 x ran z z + M
168 167 ex φ x M + 1 x ran z z + M
169 168 ssrdv φ M + 1 ran z z + M
170 imass2 M + 1 ran z z + M G M + 1 G ran z z + M
171 169 170 syl φ G M + 1 G ran z z + M
172 rnco2 ran G z z + M = G ran z z + M
173 7 130 cofmpt φ G z z + M = z G z + M
174 173 rneqd φ ran G z z + M = ran z G z + M
175 172 174 syl5eqr φ G ran z z + M = ran z G z + M
176 171 175 sseqtrd φ G M + 1 ran z G z + M
177 imass2 G M + 1 ran z G z + M . G M + 1 . ran z G z + M
178 176 177 syl φ . G M + 1 . ran z G z + M
179 imaco . G M + 1 = . G M + 1
180 rnco2 ran . z G z + M = . ran z G z + M
181 178 179 180 3sstr4g φ . G M + 1 ran . z G z + M
182 181 unissd φ . G M + 1 ran . z G z + M
183 135 ovollb z G z + M : 2 . G M + 1 ran . z G z + M vol * . G M + 1 sup ran seq 1 + abs z G z + M * <
184 133 182 183 syl2anc φ vol * . G M + 1 sup ran seq 1 + abs z G z + M * <
185 123 frnd φ ran T 0 +∞
186 185 139 sstrdi φ ran T *
187 9 fveq1i T M + n = seq 1 + abs G M + n
188 11 nnred φ M
189 188 ltp1d φ M < M + 1
190 fzdisj M < M + 1 1 M M + 1 M + n =
191 189 190 syl φ 1 M M + 1 M + n =
192 191 adantr φ n 1 M M + 1 M + n =
193 nnnn0 n n 0
194 nn0addge1 M n 0 M M + n
195 188 193 194 syl2an φ n M M + n
196 11 adantr φ n M
197 196 67 eleqtrdi φ n M 1
198 nnaddcl M n M + n
199 11 198 sylan φ n M + n
200 199 nnzd φ n M + n
201 elfz5 M 1 M + n M 1 M + n M M + n
202 197 200 201 syl2anc φ n M 1 M + n M M + n
203 195 202 mpbird φ n M 1 M + n
204 fzsplit M 1 M + n 1 M + n = 1 M M + 1 M + n
205 203 204 syl φ n 1 M + n = 1 M M + 1 M + n
206 fzfid φ n 1 M + n Fin
207 7 adantr φ n G : 2
208 elfznn j 1 M + n j
209 ovolfcl G : 2 j 1 st G j 2 nd G j 1 st G j 2 nd G j
210 207 208 209 syl2an φ n j 1 M + n 1 st G j 2 nd G j 1 st G j 2 nd G j
211 210 simp2d φ n j 1 M + n 2 nd G j
212 210 simp1d φ n j 1 M + n 1 st G j
213 211 212 resubcld φ n j 1 M + n 2 nd G j 1 st G j
214 213 recnd φ n j 1 M + n 2 nd G j 1 st G j
215 192 205 206 214 fsumsplit φ n j = 1 M + n 2 nd G j 1 st G j = j = 1 M 2 nd G j 1 st G j + j = M + 1 M + n 2 nd G j 1 st G j
216 121 ovolfsval G : 2 j abs G j = 2 nd G j 1 st G j
217 207 208 216 syl2an φ n j 1 M + n abs G j = 2 nd G j 1 st G j
218 199 67 eleqtrdi φ n M + n 1
219 217 218 214 fsumser φ n j = 1 M + n 2 nd G j 1 st G j = seq 1 + abs G M + n
220 7 ad2antrr φ n j 1 M G : 2
221 32 adantl φ n j 1 M j
222 220 221 216 syl2anc φ n j 1 M abs G j = 2 nd G j 1 st G j
223 7 32 209 syl2an φ j 1 M 1 st G j 2 nd G j 1 st G j 2 nd G j
224 223 simp2d φ j 1 M 2 nd G j
225 223 simp1d φ j 1 M 1 st G j
226 224 225 resubcld φ j 1 M 2 nd G j 1 st G j
227 226 adantlr φ n j 1 M 2 nd G j 1 st G j
228 227 recnd φ n j 1 M 2 nd G j 1 st G j
229 222 197 228 fsumser φ n j = 1 M 2 nd G j 1 st G j = seq 1 + abs G M
230 9 fveq1i T M = seq 1 + abs G M
231 229 230 syl6eqr φ n j = 1 M 2 nd G j 1 st G j = T M
232 196 nnzd φ n M
233 232 peano2zd φ n M + 1
234 7 ad2antrr φ n j M + 1 M + n G : 2
235 196 peano2nnd φ n M + 1
236 elfzuz j M + 1 M + n j M + 1
237 eluznn M + 1 j M + 1 j
238 235 236 237 syl2an φ n j M + 1 M + n j
239 234 238 209 syl2anc φ n j M + 1 M + n 1 st G j 2 nd G j 1 st G j 2 nd G j
240 239 simp2d φ n j M + 1 M + n 2 nd G j
241 239 simp1d φ n j M + 1 M + n 1 st G j
242 240 241 resubcld φ n j M + 1 M + n 2 nd G j 1 st G j
243 242 recnd φ n j M + 1 M + n 2 nd G j 1 st G j
244 2fveq3 j = k + M 2 nd G j = 2 nd G k + M
245 2fveq3 j = k + M 1 st G j = 1 st G k + M
246 244 245 oveq12d j = k + M 2 nd G j 1 st G j = 2 nd G k + M 1 st G k + M
247 232 233 200 243 246 fsumshftm φ n j = M + 1 M + n 2 nd G j 1 st G j = k = M + 1 - M M + n - M 2 nd G k + M 1 st G k + M
248 196 nncnd φ n M
249 pncan2 M 1 M + 1 - M = 1
250 248 74 249 sylancl φ n M + 1 - M = 1
251 nncn n n
252 251 adantl φ n n
253 248 252 pncan2d φ n M + n - M = n
254 250 253 oveq12d φ n M + 1 - M M + n - M = 1 n
255 254 sumeq1d φ n k = M + 1 - M M + n - M 2 nd G k + M 1 st G k + M = k = 1 n 2 nd G k + M 1 st G k + M
256 133 adantr φ n z G z + M : 2
257 elfznn k 1 n k
258 134 ovolfsval z G z + M : 2 k abs z G z + M k = 2 nd z G z + M k 1 st z G z + M k
259 256 257 258 syl2an φ n k 1 n abs z G z + M k = 2 nd z G z + M k 1 st z G z + M k
260 257 adantl φ n k 1 n k
261 fvoveq1 z = k G z + M = G k + M
262 eqid z G z + M = z G z + M
263 fvex G k + M V
264 261 262 263 fvmpt k z G z + M k = G k + M
265 260 264 syl φ n k 1 n z G z + M k = G k + M
266 265 fveq2d φ n k 1 n 2 nd z G z + M k = 2 nd G k + M
267 265 fveq2d φ n k 1 n 1 st z G z + M k = 1 st G k + M
268 266 267 oveq12d φ n k 1 n 2 nd z G z + M k 1 st z G z + M k = 2 nd G k + M 1 st G k + M
269 259 268 eqtrd φ n k 1 n abs z G z + M k = 2 nd G k + M 1 st G k + M
270 simpr φ n n
271 270 67 eleqtrdi φ n n 1
272 7 ad2antrr φ n k 1 n G : 2
273 nnaddcl k M k + M
274 257 196 273 syl2anr φ n k 1 n k + M
275 ovolfcl G : 2 k + M 1 st G k + M 2 nd G k + M 1 st G k + M 2 nd G k + M
276 272 274 275 syl2anc φ n k 1 n 1 st G k + M 2 nd G k + M 1 st G k + M 2 nd G k + M
277 276 simp2d φ n k 1 n 2 nd G k + M
278 276 simp1d φ n k 1 n 1 st G k + M
279 277 278 resubcld φ n k 1 n 2 nd G k + M 1 st G k + M
280 279 recnd φ n k 1 n 2 nd G k + M 1 st G k + M
281 269 271 280 fsumser φ n k = 1 n 2 nd G k + M 1 st G k + M = seq 1 + abs z G z + M n
282 247 255 281 3eqtrd φ n j = M + 1 M + n 2 nd G j 1 st G j = seq 1 + abs z G z + M n
283 231 282 oveq12d φ n j = 1 M 2 nd G j 1 st G j + j = M + 1 M + n 2 nd G j 1 st G j = T M + seq 1 + abs z G z + M n
284 215 219 283 3eqtr3d φ n seq 1 + abs G M + n = T M + seq 1 + abs z G z + M n
285 187 284 syl5eq φ n T M + n = T M + seq 1 + abs z G z + M n
286 123 ffnd φ T Fn
287 fnfvelrn T Fn M + n T M + n ran T
288 286 199 287 syl2an2r φ n T M + n ran T
289 285 288 eqeltrrd φ n T M + seq 1 + abs z G z + M n ran T
290 supxrub ran T * T M + seq 1 + abs z G z + M n ran T T M + seq 1 + abs z G z + M n sup ran T * <
291 186 289 290 syl2an2r φ n T M + seq 1 + abs z G z + M n sup ran T * <
292 125 adantr φ n T M
293 137 ffvelrnda φ n seq 1 + abs z G z + M n 0 +∞
294 120 293 sseldi φ n seq 1 + abs z G z + M n
295 90 adantr φ n sup ran T * <
296 292 294 295 leaddsub2d φ n T M + seq 1 + abs z G z + M n sup ran T * < seq 1 + abs z G z + M n sup ran T * < T M
297 291 296 mpbid φ n seq 1 + abs z G z + M n sup ran T * < T M
298 297 ralrimiva φ n seq 1 + abs z G z + M n sup ran T * < T M
299 137 ffnd φ seq 1 + abs z G z + M Fn
300 breq1 x = seq 1 + abs z G z + M n x sup ran T * < T M seq 1 + abs z G z + M n sup ran T * < T M
301 300 ralrn seq 1 + abs z G z + M Fn x ran seq 1 + abs z G z + M x sup ran T * < T M n seq 1 + abs z G z + M n sup ran T * < T M
302 299 301 syl φ x ran seq 1 + abs z G z + M x sup ran T * < T M n seq 1 + abs z G z + M n sup ran T * < T M
303 298 302 mpbird φ x ran seq 1 + abs z G z + M x sup ran T * < T M
304 supxrleub ran seq 1 + abs z G z + M * sup ran T * < T M * sup ran seq 1 + abs z G z + M * < sup ran T * < T M x ran seq 1 + abs z G z + M x sup ran T * < T M
305 140 143 304 syl2anc φ sup ran seq 1 + abs z G z + M * < sup ran T * < T M x ran seq 1 + abs z G z + M x sup ran T * < T M
306 303 305 mpbird φ sup ran seq 1 + abs z G z + M * < sup ran T * < T M
307 127 142 143 184 306 xrletrd φ vol * . G M + 1 sup ran T * < T M
308 125 90 50 absdifltd φ T M sup ran T * < < C sup ran T * < C < T M T M < sup ran T * < + C
309 12 308 mpbid φ sup ran T * < C < T M T M < sup ran T * < + C
310 309 simpld φ sup ran T * < C < T M
311 90 50 125 310 ltsub23d φ sup ran T * < T M < C
312 97 126 50 307 311 lelttrd φ vol * . G M + 1 < C
313 97 50 49 312 ltadd2dd φ vol * K A + vol * . G M + 1 < vol * K A + C
314 23 98 51 119 313 lelttrd φ vol * E A < vol * K A + C
315 54 97 readdcld φ vol * K A + vol * . G M + 1
316 difss K A K
317 unss1 K A K K A . G M + 1 K . G M + 1
318 316 317 ax-mp K A . G M + 1 K . G M + 1
319 318 88 sseqtrrid φ K A . G M + 1 ran . G
320 ovolsscl K A . G M + 1 ran . G ran . G vol * ran . G vol * K A . G M + 1
321 319 20 95 320 syl3anc φ vol * K A . G M + 1
322 104 ssdifd φ E A K . G M + 1 A
323 difundir K . G M + 1 A = K A . G M + 1 A
324 difss . G M + 1 A . G M + 1
325 unss2 . G M + 1 A . G M + 1 K A . G M + 1 A K A . G M + 1
326 324 325 ax-mp K A . G M + 1 A K A . G M + 1
327 323 326 eqsstri K . G M + 1 A K A . G M + 1
328 322 327 sstrdi φ E A K A . G M + 1
329 319 20 sstrd φ K A . G M + 1
330 ovolss E A K A . G M + 1 K A . G M + 1 vol * E A vol * K A . G M + 1
331 328 329 330 syl2anc φ vol * E A vol * K A . G M + 1
332 52 46 sstrd φ K A
333 ovolun K A vol * K A . G M + 1 vol * . G M + 1 vol * K A . G M + 1 vol * K A + vol * . G M + 1
334 332 54 116 97 333 syl22anc φ vol * K A . G M + 1 vol * K A + vol * . G M + 1
335 26 321 315 331 334 letrd φ vol * E A vol * K A + vol * . G M + 1
336 97 50 54 312 ltadd2dd φ vol * K A + vol * . G M + 1 < vol * K A + C
337 26 315 55 335 336 lelttrd φ vol * E A < vol * K A + C
338 23 26 51 55 314 337 lt2addd φ vol * E A + vol * E A < vol * K A + C + vol * K A + C
339 49 recnd φ vol * K A
340 50 recnd φ C
341 54 recnd φ vol * K A
342 339 340 341 340 add4d φ vol * K A + C + vol * K A + C = vol * K A + vol * K A + C + C
343 338 342 breqtrd φ vol * E A + vol * E A < vol * K A + vol * K A + C + C