Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2monolem1 Structured version   Unicode version

Theorem itg2monolem1 19634
 Description: Lemma for itg2mono 19637. We show that for any constant less than one, is less than , and so , which is one half of the equality in itg2mono 19637. Consider the sequence . This is an increasing sequence of measurable sets whose union is , and so has an integral which equals in the limit, by itg1climres 19598. Then by taking the limit in , we get as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
itg2mono.1
itg2mono.2 MblFn
itg2mono.3
itg2mono.4
itg2mono.5
itg2mono.6
itg2mono.7
itg2mono.8
itg2mono.9
itg2mono.10
itg2mono.11
Assertion
Ref Expression
itg2monolem1
Distinct variable groups:   ,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,)

Proof of Theorem itg2monolem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10513 . 2
2 1z 10303 . . 3
32a1i 11 . 2
4 readdcl 9065 . . . . . . . . . . . . . . . 16
54adantl 453 . . . . . . . . . . . . . . 15
6 itg2mono.3 . . . . . . . . . . . . . . . 16
7 0re 9083 . . . . . . . . . . . . . . . . 17
8 pnfxr 10705 . . . . . . . . . . . . . . . . 17
9 icossre 10983 . . . . . . . . . . . . . . . . 17
107, 8, 9mp2an 654 . . . . . . . . . . . . . . . 16
11 fss 5591 . . . . . . . . . . . . . . . 16
126, 10, 11sylancl 644 . . . . . . . . . . . . . . 15
13 itg2mono.8 . . . . . . . . . . . . . . . . . 18
14 itg2mono.7 . . . . . . . . . . . . . . . . . . . . 21
15 0xr 9123 . . . . . . . . . . . . . . . . . . . . . 22
16 1re 9082 . . . . . . . . . . . . . . . . . . . . . . 23
1716rexri 9129 . . . . . . . . . . . . . . . . . . . . . 22
18 elioo2 10949 . . . . . . . . . . . . . . . . . . . . . 22
1915, 17, 18mp2an 654 . . . . . . . . . . . . . . . . . . . . 21
2014, 19sylib 189 . . . . . . . . . . . . . . . . . . . 20
2120simp1d 969 . . . . . . . . . . . . . . . . . . 19
2221renegcld 9456 . . . . . . . . . . . . . . . . . 18
2313, 22i1fmulc 19587 . . . . . . . . . . . . . . . . 17
2423adantr 452 . . . . . . . . . . . . . . . 16
25 i1ff 19560 . . . . . . . . . . . . . . . 16
2624, 25syl 16 . . . . . . . . . . . . . . 15
27 reex 9073 . . . . . . . . . . . . . . . 16
2827a1i 11 . . . . . . . . . . . . . . 15
29 inidm 3542 . . . . . . . . . . . . . . 15
305, 12, 26, 28, 28, 29off 6312 . . . . . . . . . . . . . 14
3130adantr 452 . . . . . . . . . . . . 13
32 ffn 5583 . . . . . . . . . . . . 13
3331, 32syl 16 . . . . . . . . . . . 12
34 elpreima 5842 . . . . . . . . . . . 12
3533, 34syl 16 . . . . . . . . . . 11
36 simpr 448 . . . . . . . . . . . 12
3736biantrurd 495 . . . . . . . . . . 11
3835, 37bitr4d 248 . . . . . . . . . 10
3930ffvelrnda 5862 . . . . . . . . . . . 12
4039biantrurd 495 . . . . . . . . . . 11
41 elioomnf 10991 . . . . . . . . . . . 12
4215, 41ax-mp 8 . . . . . . . . . . 11
4340, 42syl6rbbr 256 . . . . . . . . . 10
44 ffn 5583 . . . . . . . . . . . . . . 15
4512, 44syl 16 . . . . . . . . . . . . . 14
46 ffn 5583 . . . . . . . . . . . . . . 15
4726, 46syl 16 . . . . . . . . . . . . . 14
48 eqidd 2436 . . . . . . . . . . . . . 14
4922adantr 452 . . . . . . . . . . . . . . . 16
50 i1ff 19560 . . . . . . . . . . . . . . . . . . 19
5113, 50syl 16 . . . . . . . . . . . . . . . . . 18
52 ffn 5583 . . . . . . . . . . . . . . . . . 18
5351, 52syl 16 . . . . . . . . . . . . . . . . 17
5453adantr 452 . . . . . . . . . . . . . . . 16
55 eqidd 2436 . . . . . . . . . . . . . . . 16
5628, 49, 54, 55ofc1 6319 . . . . . . . . . . . . . . 15
5721recnd 9106 . . . . . . . . . . . . . . . . 17
5857ad2antrr 707 . . . . . . . . . . . . . . . 16
5951ffvelrnda 5862 . . . . . . . . . . . . . . . . . 18
6059adantlr 696 . . . . . . . . . . . . . . . . 17
6160recnd 9106 . . . . . . . . . . . . . . . 16
6258, 61mulneg1d 9478 . . . . . . . . . . . . . . 15
6356, 62eqtrd 2467 . . . . . . . . . . . . . 14
6445, 47, 28, 28, 29, 48, 63ofval 6306 . . . . . . . . . . . . 13
6512ffvelrnda 5862 . . . . . . . . . . . . . . 15
6665recnd 9106 . . . . . . . . . . . . . 14
6721adantr 452 . . . . . . . . . . . . . . . . 17
6867, 59remulcld 9108 . . . . . . . . . . . . . . . 16
6968adantlr 696 . . . . . . . . . . . . . . 15
7069recnd 9106 . . . . . . . . . . . . . 14
7166, 70negsubd 9409 . . . . . . . . . . . . 13
7264, 71eqtrd 2467 . . . . . . . . . . . 12
7372breq1d 4214 . . . . . . . . . . 11
747a1i 11 . . . . . . . . . . . 12
7565, 69, 74ltsubaddd 9614 . . . . . . . . . . 11
7670addid2d 9259 . . . . . . . . . . . 12
7776breq2d 4216 . . . . . . . . . . 11
7873, 75, 773bitrd 271 . . . . . . . . . 10
7938, 43, 783bitrd 271 . . . . . . . . 9
8079notbid 286 . . . . . . . 8
81 eldif 3322 . . . . . . . . . 10
8281baib 872 . . . . . . . . 9
8382adantl 453 . . . . . . . 8
8469, 65lenltd 9211 . . . . . . . 8
8580, 83, 843bitr4d 277 . . . . . . 7
8685rabbi2dva 3541 . . . . . 6
87 rembl 19427 . . . . . . 7
88 itg2mono.2 . . . . . . . . . 10 MblFn
89 i1fmbf 19559 . . . . . . . . . . 11 MblFn
9024, 89syl 16 . . . . . . . . . 10 MblFn
9188, 90mbfadd 19545 . . . . . . . . 9 MblFn
92 mbfima 19516 . . . . . . . . 9 MblFn
9391, 30, 92syl2anc 643 . . . . . . . 8
94 cmmbl 19421 . . . . . . . 8
9593, 94syl 16 . . . . . . 7
96 inmbl 19428 . . . . . . 7
9787, 95, 96sylancr 645 . . . . . 6
9886, 97eqeltrrd 2510 . . . . 5
99 itg2mono.11 . . . . 5
10098, 99fmptd 5885 . . . 4
101 itg2mono.4 . . . . . . . . . . . 12
102101ralrimiva 2781 . . . . . . . . . . 11
103 fveq2 5720 . . . . . . . . . . . . 13
104 oveq1 6080 . . . . . . . . . . . . . 14
105104fveq2d 5724 . . . . . . . . . . . . 13
106103, 105breq12d 4217 . . . . . . . . . . . 12
107106cbvralv 2924 . . . . . . . . . . 11
108102, 107sylib 189 . . . . . . . . . 10
109108r19.21bi 2796 . . . . . . . . 9
1106ralrimiva 2781 . . . . . . . . . . . . 13
111103feq1d 5572 . . . . . . . . . . . . . 14
112111cbvralv 2924 . . . . . . . . . . . . 13
113110, 112sylib 189 . . . . . . . . . . . 12
114113r19.21bi 2796 . . . . . . . . . . 11
115 ffn 5583 . . . . . . . . . . 11
116114, 115syl 16 . . . . . . . . . 10
117 peano2nn 10004 . . . . . . . . . . . 12
118 fveq2 5720 . . . . . . . . . . . . . 14
119118feq1d 5572 . . . . . . . . . . . . 13
120119rspccva 3043 . . . . . . . . . . . 12
121110, 117, 120syl2an 464 . . . . . . . . . . 11
122 ffn 5583 . . . . . . . . . . 11
123121, 122syl 16 . . . . . . . . . 10
12427a1i 11 . . . . . . . . . 10
125 eqidd 2436 . . . . . . . . . 10
126 eqidd 2436 . . . . . . . . . 10
127116, 123, 124, 124, 29, 125, 126ofrfval 6305 . . . . . . . . 9
128109, 127mpbid 202 . . . . . . . 8
129128r19.21bi 2796 . . . . . . 7
13021ad2antrr 707 . . . . . . . . 9
13151adantr 452 . . . . . . . . . 10
132131ffvelrnda 5862 . . . . . . . . 9
133130, 132remulcld 9108 . . . . . . . 8
134 fss 5591 . . . . . . . . . 10
135114, 10, 134sylancl 644 . . . . . . . . 9
136135ffvelrnda 5862 . . . . . . . 8
137 fss 5591 . . . . . . . . . 10
138121, 10, 137sylancl 644 . . . . . . . . 9
139138ffvelrnda 5862 . . . . . . . 8
140 letr 9159 . . . . . . . 8
141133, 136, 139, 140syl3anc 1184 . . . . . . 7
142129, 141mpan2d 656 . . . . . 6
143142ss2rabdv 3416 . . . . 5
144103fveq1d 5722 . . . . . . . . 9
145144breq2d 4216 . . . . . . . 8
146145rabbidv 2940 . . . . . . 7
14727rabex 4346 . . . . . . 7
148146, 99, 147fvmpt 5798 . . . . . 6
149148adantl 453 . . . . 5
150117adantl 453 . . . . . 6
151118fveq1d 5722 . . . . . . . . 9
152151breq2d 4216 . . . . . . . 8
153152rabbidv 2940 . . . . . . 7
15427rabex 4346 . . . . . . 7
155153, 99, 154fvmpt 5798 . . . . . 6
156150, 155syl 16 . . . . 5
157143, 149, 1563sstr4d 3383 . . . 4
15868adantrr 698 . . . . . . . . . . . . . 14
15959adantrr 698 . . . . . . . . . . . . . 14
16065an32s 780 . . . . . . . . . . . . . . . . . 18
161 eqid 2435 . . . . . . . . . . . . . . . . . 18
162160, 161fmptd 5885 . . . . . . . . . . . . . . . . 17
163 frn 5589 . . . . . . . . . . . . . . . . 17
164162, 163syl 16 . . . . . . . . . . . . . . . 16
165 1nn 10003 . . . . . . . . . . . . . . . . . . 19
166 fdm 5587 . . . . . . . . . . . . . . . . . . . 20
167162, 166syl 16 . . . . . . . . . . . . . . . . . . 19
168165, 167syl5eleqr 2522 . . . . . . . . . . . . . . . . . 18
169 ne0i 3626 . . . . . . . . . . . . . . . . . 18
170168, 169syl 16 . . . . . . . . . . . . . . . . 17
171 dm0rn0 5078 . . . . . . . . . . . . . . . . . 18
172171necon3bii 2630 . . . . . . . . . . . . . . . . 17
173170, 172sylib 189 . . . . . . . . . . . . . . . 16
174 itg2mono.5 . . . . . . . . . . . . . . . . 17
175 ffn 5583 . . . . . . . . . . . . . . . . . . . . 21
176162, 175syl 16 . . . . . . . . . . . . . . . . . . . 20
177 breq1 4207 . . . . . . . . . . . . . . . . . . . . 21
178177ralrn 5865 . . . . . . . . . . . . . . . . . . . 20
179176, 178syl 16 . . . . . . . . . . . . . . . . . . 19
180 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . 24
181180fveq1d 5722 . . . . . . . . . . . . . . . . . . . . . . 23
182 fvex 5734 . . . . . . . . . . . . . . . . . . . . . . 23
183181, 161, 182fvmpt 5798 . . . . . . . . . . . . . . . . . . . . . 22
184183breq1d 4214 . . . . . . . . . . . . . . . . . . . . 21
185184ralbiia 2729 . . . . . . . . . . . . . . . . . . . 20
186181breq1d 4214 . . . . . . . . . . . . . . . . . . . . 21
187186cbvralv 2924 . . . . . . . . . . . . . . . . . . . 20
188185, 187bitr4i 244 . . . . . . . . . . . . . . . . . . 19
189179, 188syl6bb 253 . . . . . . . . . . . . . . . . . 18
190189rexbidv 2718 . . . . . . . . . . . . . . . . 17
191174, 190mpbird 224 . . . . . . . . . . . . . . . 16
192 suprcl 9960 . . . . . . . . . . . . . . . 16
193164, 173, 191, 192syl3anc 1184 . . . . . . . . . . . . . . 15
194193adantrr 698 . . . . . . . . . . . . . 14
19520simp3d 971 . . . . . . . . . . . . . . . . 17
196195adantr 452 . . . . . . . . . . . . . . . 16
19721adantr 452 . . . . . . . . . . . . . . . . 17
19816a1i 11 . . . . . . . . . . . . . . . . 17
199 simprr 734 . . . . . . . . . . . . . . . . 17
200 ltmul1 9852 . . . . . . . . . . . . . . . . 17
201197, 198, 159, 199, 200syl112anc 1188 . . . . . . . . . . . . . . . 16
202196, 201mpbid 202 . . . . . . . . . . . . . . 15
203159recnd 9106 . . . . . . . . . . . . . . . 16
204203mulid2d 9098 . . . . . . . . . . . . . . 15
205202, 204breqtrd 4228 . . . . . . . . . . . . . 14
206 itg2mono.9 . . . . . . . . . . . . . . . . . 18
207 itg2mono.1 . . . . . . . . . . . . . . . . . . . . 21
208193, 207fmptd 5885 . . . . . . . . . . . . . . . . . . . 20
209 ffn 5583 . . . . . . . . . . . . . . . . . . . 20
210208, 209syl 16 . . . . . . . . . . . . . . . . . . 19
21127a1i 11 . . . . . . . . . . . . . . . . . . 19
212 eqidd 2436 . . . . . . . . . . . . . . . . . . 19
213 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . 24
214213mpteq2dv 4288 . . . . . . . . . . . . . . . . . . . . . . 23
215214rneqd 5089 . . . . . . . . . . . . . . . . . . . . . 22
216215supeq1d 7443 . . . . . . . . . . . . . . . . . . . . 21
217 ltso 9148 . . . . . . . . . . . . . . . . . . . . . 22
218217supex 7460 . . . . . . . . . . . . . . . . . . . . 21
219216, 207, 218fvmpt 5798 . . . . . . . . . . . . . . . . . . . 20
220219adantl 453 . . . . . . . . . . . . . . . . . . 19
22153, 210, 211, 211, 29, 212, 220ofrfval 6305 . . . . . . . . . . . . . . . . . 18
222206, 221mpbid 202 . . . . . . . . . . . . . . . . 17
223 fveq2 5720 . . . . . . . . . . . . . . . . . . 19
224223, 216breq12d 4217 . . . . . . . . . . . . . . . . . 18
225224cbvralv 2924 . . . . . . . . . . . . . . . . 17
226222, 225sylibr 204 . . . . . . . . . . . . . . . 16
227226r19.21bi 2796 . . . . . . . . . . . . . . 15
228227adantrr 698 . . . . . . . . . . . . . 14
229158, 159, 194, 205, 228ltletrd 9222 . . . . . . . . . . . . 13
230164adantrr 698 . . . . . . . . . . . . . 14
231173adantrr 698 . . . . . . . . . . . . . 14
232191adantrr 698 . . . . . . . . . . . . . 14
233 suprlub 9962 . . . . . . . . . . . . . 14
234230, 231, 232, 158, 233syl31anc 1187 . . . . . . . . . . . . 13
235229, 234mpbid 202 . . . . . . . . . . . 12
236176adantrr 698 . . . . . . . . . . . . . 14
237 breq2 4208 . . . . . . . . . . . . . . 15
238237rexrn 5864 . . . . . . . . . . . . . 14
239236, 238syl 16 . . . . . . . . . . . . 13
240 fvex 5734 . . . . . . . . . . . . . . . 16
241144, 161, 240fvmpt 5798 . . . . . . . . . . . . . . 15
242241breq2d 4216 . . . . . . . . . . . . . 14
243242rexbiia 2730 . . . . . . . . . . . . 13
244239, 243syl6bb 253 . . . . . . . . . . . 12
245235, 244mpbid 202 . . . . . . . . . . 11
246197, 159remulcld 9108 . . . . . . . . . . . . . 14
247246adantr 452 . . . . . . . . . . . . 13
248114adantlr 696 . . . . . . . . . . . . . . . . 17
249 simplr 732 . . . . . . . . . . . . . . . . 17
250248, 249ffvelrnd 5863 . . . . . . . . . . . . . . . 16
251 elrege0 10999 . . . . . . . . . . . . . . . 16
252250, 251sylib 189 . . . . . . . . . . . . . . 15
253252simpld 446 . . . . . . . . . . . . . 14
254253adantlrr 702 . . . . . . . . . . . . 13
255 ltle 9155 . . . . . . . . . . . . 13
256247, 254, 255syl2anc 643 . . . . . . . . . . . 12
257256reximdva 2810 . . . . . . . . . . 11
258245, 257mpd 15 . . . . . . . . . 10
259258anassrs 630 . . . . . . . . 9
260 ne0i 3626 . . . . . . . . . . . 12
261165, 260ax-mp 8 . . . . . . . . . . 11
26268adantrr 698 . . . . . . . . . . . . . 14
263262adantr 452 . . . . . . . . . . . . 13
2647a1i 11 . . . . . . . . . . . . 13
265252adantlrr 702 . . . . . . . . . . . . . 14
266265simpld 446 . . . . . . . . . . . . 13
267 simplrr 738 . . . . . . . . . . . . . . 15
26859adantrr 698 . . . . . . . . . . . . . . . . 17
269268adantr 452 . . . . . . . . . . . . . . . 16
27021ad2antrr 707 . . . . . . . . . . . . . . . 16
27120simp2d 970 . . . . . . . . . . . . . . . . 17
272271ad2antrr 707 . . . . . . . . . . . . . . . 16
273 lemul2 9855 . . . . . . . . . . . . . . . 16
274269, 264, 270, 272, 273syl112anc 1188 . . . . . . . . . . . . . . 15
275267, 274mpbid 202 . . . . . . . . . . . . . 14
276270recnd 9106 . . . . . . . . . . . . . . 15
277276mul01d 9257 . . . . . . . . . . . . . 14
278275, 277breqtrd 4228 . . . . . . . . . . . . 13
279265simprd 450 . . . . . . . . . . . . 13
280263, 264, 266, 278, 279letrd 9219 . . . . . . . . . . . 12
281280ralrimiva 2781 . . . . . . . . . . 11
282 r19.2z 3709 . . . . . . . . . . 11
283261, 281, 282sylancr 645 . . . . . . . . . 10
284283anassrs 630 . . . . . . . . 9
2857a1i 11 . . . . . . . . 9
286259, 284, 285, 59ltlecasei 9173 . . . . . . . 8
287286ralrimiva 2781 . . . . . . 7
288 rabid2 2877 . . . . . . 7
289287, 288sylibr 204 . . . . . 6
290 iunrab 4130 . . . . . 6
291289, 290syl6eqr 2485 . . . . 5
292149iuneq2dv 4106 . . . . 5
293 ffn 5583 . . . . . . 7
294100, 293syl 16 . . . . . 6
295 fniunfv 5986 . . . . . 6
296294, 295syl 16 . . . . 5
297291, 292, 2963eqtr2rd 2474 . . . 4
298 eqid 2435 . . . 4
299100, 157, 297, 13, 298itg1climres 19598 . . 3
300 nnex 9998 . . . . 5
301300mptex 5958 . . . 4
302301a1i 11 . . 3
303 fveq2 5720 . . . . . . . . . . 11
304303eleq2d 2502 . . . . . . . . . 10
305304ifbid 3749 . . . . . . . . 9
306305mpteq2dv 4288 . . . . . . . 8
307306fveq2d 5724 . . . . . . 7
308 eqid 2435 . . . . . . 7
309 fvex 5734 . . . . . . 7
310307, 308, 309fvmpt 5798 . . . . . 6
311310adantl 453 . . . . 5
31213adantr 452 . . . . . . 7
313100ffvelrnda 5862 . . . . . . 7
314 eqid 2435 . . . . . . . 8
315314i1fres 19589 . . . . . . 7
316312, 313, 315syl2anc 643 . . . . . 6
317 itg1cl 19569 . . . . . 6
318316, 317syl 16 . . . . 5
319311, 318eqeltrd 2509 . . . 4
320319recnd 9106 . . 3
321307oveq2d 6089 . . . . . 6
322 eqid 2435 . . . . . 6
323 ovex 6098 . . . . . 6
324321, 322, 323fvmpt 5798 . . . . 5
325310oveq2d 6089 . . . . 5
326324, 325eqtr4d 2470 . . . 4
3281, 3, 299, 57, 302, 320, 327climmulc2 12422 . 2
329 rexr 9122 . . . . . . . . . 10
330329anim1i 552 . . . . . . . . 9
331 elrege0 10999 . . . . . . . . 9
332 elxrge0 11000 . . . . . . . . 9
333330, 331, 3323imtr4i 258 . . . . . . . 8
334333ssriv 3344 . . . . . . 7
335 fss 5591 . . . . . . 7
3366, 334, 335sylancl 644 . . . . . 6
337 itg2mono.10 . . . . . . 7
338337adantr 452 . . . . . 6
339 itg2cl 19616 . . . . . . . . . . . 12
340336, 339syl 16 . . . . . . . . . . 11
341 eqid 2435 . . . . . . . . . . 11
342340, 341fmptd 5885 . . . . . . . . . 10
343 frn 5589 . . . . . . . . . 10
344342, 343syl 16 . . . . . . . . 9
345344adantr 452 . . . . . . . 8
346 fvex 5734 . . . . . . . . . . 11
347346elabrex 5977 . . . . . . . . . 10
348347adantl 453 . . . . . . . . 9
349341rnmpt 5108 . . . . . . . . 9
350348, 349syl6eleqr 2526 . . . . . . . 8
351 supxrub 10895 . . . . . . . 8
352345, 350, 351syl2anc 643 . . . . . . 7
353 itg2mono.6 . . . . . . 7
354352, 353syl6breqr 4244 . . . . . 6
355 itg2lecl 19622 . . . . . 6
356336, 338, 354, 355syl3anc 1184 . . . . 5
357356, 341fmptd 5885 . . . 4
358336ralrimiva 2781 . . . . . . . . . 10
359 fveq2 5720 . . . . . . . . . . . 12
360359feq1d 5572 . . . . . . . . . . 11
361360cbvralv 2924 . . . . . . . . . 10
362358, 361sylib 189 . . . . . . . . 9
363 peano2nn 10004 . . . . . . . . 9
364 fveq2 5720 . . . . . . . . . . 11
365364feq1d 5572 . . . . . . . . . 10
366365rspccva 3043 . . . . . . . . 9
367362, 363, 366syl2an 464 . . . . . . . 8
368 itg2le 19623 . . . . . . . 8
369336, 367, 101, 368syl3anc 1184 . . . . . . 7
370369ralrimiva 2781 . . . . . 6
371359fveq2d 5724 . . . . . . . . . 10
372 fvex 5734 . . . . . . . . . 10
373371, 341, 372fvmpt 5798 . . . . . . . . 9
374 peano2nn 10004 . . . . . . . . . 10
375 fveq2 5720 . . . . . . . . . . . 12
376375fveq2d 5724 . . . . . . . . . . 11
377 fvex 5734 . . . . . . . . . . 11
378376, 341, 377fvmpt 5798 . . . . . . . . . 10
379374, 378syl 16 . . . . . . . . 9
380373, 379breq12d 4217 . . . . . . . 8
381380ralbiia 2729 . . . . . . 7
382 oveq1 6080 . . . . . . . . . . 11
383382fveq2d 5724 . . . . . . . . . 10
384383fveq2d 5724 . . . . . . . . 9
385371, 384breq12d 4217 . . . . . . . 8
386385cbvralv 2924 . . . . . . 7
387381, 386bitr4i 244 . . . . . 6
388370, 387sylibr 204 . . . . 5
389388r19.21bi 2796 . . . 4
390354ralrimiva 2781 . . . . 5
391373breq1d 4214 . . . . . . . . 9
392391ralbiia 2729 . . . . . . . 8
393371breq1d 4214 . . . . . . . . 9
394393cbvralv 2924 . . . . . . . 8
395392, 394bitr4i 244 . . . . . . 7
396 breq2 4208 . . . . . . . 8
397396ralbidv 2717 . . . . . . 7
398395, 397syl5bb 249 . . . . . 6