Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem49 Structured version   Visualization version   Unicode version

Theorem fourierdlem49 38131
 Description: The given periodic function has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem49.a
fourierdlem49.b
fourierdlem49.altb
fourierdlem49.p ..^
fourierdlem49.t
fourierdlem49.m
fourierdlem49.q
fourierdlem49.d
fourierdlem49.f
fourierdlem49.dper
fourierdlem49.per
fourierdlem49.cn ..^
fourierdlem49.l ..^ lim
fourierdlem49.x
fourierdlem49.z
fourierdlem49.e
Assertion
Ref Expression
fourierdlem49 lim
Distinct variable groups:   ,,,   ,,   ,,   ,,   ,,   ,,   ,,,   ,,,   ,,   ,,   ,   ,,   ,   ,   ,,   ,,,   ,,   ,,,
Allowed substitution hints:   (,)   ()   (,,)   (,,,,)   ()   (,,)   (,)   (,)   (,,,,)   (,)   (,,)

Proof of Theorem fourierdlem49
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem49.a . . . . . 6
2 fourierdlem49.b . . . . . 6
3 fourierdlem49.altb . . . . . 6
4 fourierdlem49.t . . . . . 6
5 fourierdlem49.e . . . . . . 7
6 ovex 6336 . . . . . . . . . 10
7 fourierdlem49.z . . . . . . . . . . 11
87fvmpt2 5972 . . . . . . . . . 10
96, 8mpan2 685 . . . . . . . . 9
109oveq2d 6324 . . . . . . . 8
1110mpteq2ia 4478 . . . . . . 7
125, 11eqtri 2493 . . . . . 6
131, 2, 3, 4, 12fourierdlem4 38085 . . . . 5
14 fourierdlem49.x . . . . 5
1513, 14ffvelrnd 6038 . . . 4
16 simpr 468 . . . . . . 7
17 fourierdlem49.q . . . . . . . . . . . . 13
18 fourierdlem49.m . . . . . . . . . . . . . 14
19 fourierdlem49.p . . . . . . . . . . . . . . 15 ..^
2019fourierdlem2 38083 . . . . . . . . . . . . . 14 ..^
2118, 20syl 17 . . . . . . . . . . . . 13 ..^
2217, 21mpbid 215 . . . . . . . . . . . 12 ..^
2322simpld 466 . . . . . . . . . . 11
24 elmapi 7511 . . . . . . . . . . 11
2523, 24syl 17 . . . . . . . . . 10
26 ffn 5739 . . . . . . . . . 10
2725, 26syl 17 . . . . . . . . 9
2827ad2antrr 740 . . . . . . . 8
29 fvelrnb 5926 . . . . . . . 8
3028, 29syl 17 . . . . . . 7
3116, 30mpbid 215 . . . . . 6
32 1zzd 10992 . . . . . . . . . . . . . . 15
33 elfzelz 11826 . . . . . . . . . . . . . . . 16
3433ad2antlr 741 . . . . . . . . . . . . . . 15
35 1e0p1 11102 . . . . . . . . . . . . . . . . 17
3635a1i 11 . . . . . . . . . . . . . . . 16
3734zred 11063 . . . . . . . . . . . . . . . . . 18
38 elfzle1 11828 . . . . . . . . . . . . . . . . . . 19
3938ad2antlr 741 . . . . . . . . . . . . . . . . . 18
40 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
4140eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . 24
4241ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . 23
43 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
4443adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
4522simprld 773 . . . . . . . . . . . . . . . . . . . . . . . . 25
4645simpld 466 . . . . . . . . . . . . . . . . . . . . . . . 24
4746ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . 23
4842, 44, 473eqtrd 2509 . . . . . . . . . . . . . . . . . . . . . 22
4948adantllr 733 . . . . . . . . . . . . . . . . . . . . 21
5049adantllr 733 . . . . . . . . . . . . . . . . . . . 20
511adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
521rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . 25
5352adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
542rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . 25
5554adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
56 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . 24
57 iocgtlb 37695 . . . . . . . . . . . . . . . . . . . . . . . 24
5853, 55, 56, 57syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . 23
5951, 58gtned 9787 . . . . . . . . . . . . . . . . . . . . . 22
6059neneqd 2648 . . . . . . . . . . . . . . . . . . . . 21
6160ad3antrrr 744 . . . . . . . . . . . . . . . . . . . 20
6250, 61pm2.65da 586 . . . . . . . . . . . . . . . . . . 19
6362neqned 2650 . . . . . . . . . . . . . . . . . 18
6437, 39, 63ne0gt0d 9789 . . . . . . . . . . . . . . . . 17
65 0zd 10973 . . . . . . . . . . . . . . . . . 18
66 zltp1le 11010 . . . . . . . . . . . . . . . . . 18
6765, 34, 66syl2anc 673 . . . . . . . . . . . . . . . . 17
6864, 67mpbid 215 . . . . . . . . . . . . . . . 16
6936, 68eqbrtrd 4416 . . . . . . . . . . . . . . 15
70 eluz2 11188 . . . . . . . . . . . . . . 15
7132, 34, 69, 70syl3anbrc 1214 . . . . . . . . . . . . . 14
72 nnuz 11218 . . . . . . . . . . . . . 14
7371, 72syl6eleqr 2560 . . . . . . . . . . . . 13
74 nnm1nn0 10935 . . . . . . . . . . . . 13
7573, 74syl 17 . . . . . . . . . . . 12
76 nn0uz 11217 . . . . . . . . . . . . 13
7776a1i 11 . . . . . . . . . . . 12
7875, 77eleqtrd 2551 . . . . . . . . . . 11
7918nnzd 11062 . . . . . . . . . . . 12
8079ad3antrrr 744 . . . . . . . . . . 11
81 peano2zm 11004 . . . . . . . . . . . . . . 15
8233, 81syl 17 . . . . . . . . . . . . . 14
8382zred 11063 . . . . . . . . . . . . 13
8433zred 11063 . . . . . . . . . . . . 13
85 elfzel2 11824 . . . . . . . . . . . . . 14
8685zred 11063 . . . . . . . . . . . . 13
8784ltm1d 10561 . . . . . . . . . . . . 13
88 elfzle2 11829 . . . . . . . . . . . . 13
8983, 84, 86, 87, 88ltletrd 9812 . . . . . . . . . . . 12
9089ad2antlr 741 . . . . . . . . . . 11
91 elfzo2 11950 . . . . . . . . . . 11 ..^
9278, 80, 90, 91syl3anbrc 1214 . . . . . . . . . 10 ..^
9325ad3antrrr 744 . . . . . . . . . . . . . 14
9434, 81syl 17 . . . . . . . . . . . . . . . . 17
9565, 80, 943jca 1210 . . . . . . . . . . . . . . . 16
9675nn0ge0d 10952 . . . . . . . . . . . . . . . 16
9783, 86, 89ltled 9800 . . . . . . . . . . . . . . . . 17
9897ad2antlr 741 . . . . . . . . . . . . . . . 16
9995, 96, 98jca32 544 . . . . . . . . . . . . . . 15
100 elfz2 11817 . . . . . . . . . . . . . . 15
10199, 100sylibr 217 . . . . . . . . . . . . . 14
10293, 101ffvelrnd 6038 . . . . . . . . . . . . 13
103102rexrd 9708 . . . . . . . . . . . 12
10425ffvelrnda 6037 . . . . . . . . . . . . . . 15
105104rexrd 9708 . . . . . . . . . . . . . 14
106105adantlr 729 . . . . . . . . . . . . 13
107106adantr 472 . . . . . . . . . . . 12
108 iocssre 11739 . . . . . . . . . . . . . . . 16
10952, 2, 108syl2anc 673 . . . . . . . . . . . . . . 15
110109sselda 3418 . . . . . . . . . . . . . 14
111110rexrd 9708 . . . . . . . . . . . . 13
112111ad2antrr 740 . . . . . . . . . . . 12
113 simplll 776 . . . . . . . . . . . . . . 15
114 ovex 6336 . . . . . . . . . . . . . . . 16
115 eleq1 2537 . . . . . . . . . . . . . . . . . 18 ..^ ..^
116115anbi2d 718 . . . . . . . . . . . . . . . . 17 ..^ ..^
117 fveq2 5879 . . . . . . . . . . . . . . . . . 18
118 oveq1 6315 . . . . . . . . . . . . . . . . . . 19
119118fveq2d 5883 . . . . . . . . . . . . . . . . . 18
120117, 119breq12d 4408 . . . . . . . . . . . . . . . . 17
121116, 120imbi12d 327 . . . . . . . . . . . . . . . 16 ..^ ..^
12222simprrd 775 . . . . . . . . . . . . . . . . 17 ..^
123122r19.21bi 2776 . . . . . . . . . . . . . . . 16 ..^
124114, 121, 123vtocl 3086 . . . . . . . . . . . . . . 15 ..^
125113, 92, 124syl2anc 673 . . . . . . . . . . . . . 14
12633zcnd 11064 . . . . . . . . . . . . . . . . . . 19
127 1cnd 9677 . . . . . . . . . . . . . . . . . . 19
128126, 127npcand 10009 . . . . . . . . . . . . . . . . . 18
129128eqcomd 2477 . . . . . . . . . . . . . . . . 17
130129fveq2d 5883 . . . . . . . . . . . . . . . 16
131130eqcomd 2477 . . . . . . . . . . . . . . 15
132131ad2antlr 741 . . . . . . . . . . . . . 14
133125, 132breqtrd 4420 . . . . . . . . . . . . 13
134 simpr 468 . . . . . . . . . . . . 13
135133, 134breqtrd 4420 . . . . . . . . . . . 12
136109, 15sseldd 3419 . . . . . . . . . . . . . . . 16
137136leidd 10201 . . . . . . . . . . . . . . 15
138137ad2antrr 740 . . . . . . . . . . . . . 14
13941adantl 473 . . . . . . . . . . . . . 14
140138, 139breqtrd 4420 . . . . . . . . . . . . 13
141140adantllr 733 . . . . . . . . . . . 12
142103, 107, 112, 135, 141eliocd 37701 . . . . . . . . . . 11
143130oveq2d 6324 . . . . . . . . . . . 12
144143ad2antlr 741 . . . . . . . . . . 11
145142, 144eleqtrd 2551 . . . . . . . . . 10
146117, 119oveq12d 6326 . . . . . . . . . . . 12
147146eleq2d 2534 . . . . . . . . . . 11
148147rspcev 3136 . . . . . . . . . 10 ..^ ..^
14992, 145, 148syl2anc 673 . . . . . . . . 9 ..^
150149ex 441 . . . . . . . 8 ..^
151150adantlr 729 . . . . . . 7 ..^
152151rexlimdva 2871 . . . . . 6 ..^
15331, 152mpd 15 . . . . 5 ..^
15418ad2antrr 740 . . . . . . 7
15525ad2antrr 740 . . . . . . 7
156 iocssicc 11747 . . . . . . . . . 10
15746eqcomd 2477 . . . . . . . . . . 11
15845simprd 470 . . . . . . . . . . . 12
159158eqcomd 2477 . . . . . . . . . . 11
160157, 159oveq12d 6326 . . . . . . . . . 10
161156, 160syl5sseq 3466 . . . . . . . . 9
162161sselda 3418 . . . . . . . 8
163162adantr 472 . . . . . . 7
164 simpr 468 . . . . . . 7
165 fveq2 5879 . . . . . . . . . 10
166165breq1d 4405 . . . . . . . . 9
167166cbvrabv 3030 . . . . . . . 8 ..^ ..^
168167supeq1i 7979 . . . . . . 7 ..^ ..^
169154, 155, 163, 164, 168fourierdlem25 38106 . . . . . 6 ..^
170 ioossioc 37684 . . . . . . . . 9
171170sseli 3414 . . . . . . . 8
172171a1i 11 . . . . . . 7 ..^
173172reximdva 2858 . . . . . 6 ..^ ..^
174169, 173mpd 15 . . . . 5 ..^
175153, 174pm2.61dan 808 . . . 4 ..^
17615, 175mpdan 681 . . 3 ..^
177 fourierdlem49.f . . . . . . . . . . 11
178 frel 5744 . . . . . . . . . . 11
179177, 178syl 17 . . . . . . . . . 10
180 resindm 5155 . . . . . . . . . . 11
181180eqcomd 2477 . . . . . . . . . 10
182179, 181syl 17 . . . . . . . . 9
183 fdm 5745 . . . . . . . . . . . 12
184177, 183syl 17 . . . . . . . . . . 11
185184ineq2d 3625 . . . . . . . . . 10
186185reseq2d 5111 . . . . . . . . 9
187182, 186eqtrd 2505 . . . . . . . 8
1881873ad2ant1 1051 . . . . . . 7 ..^
189188oveq1d 6323 . . . . . 6 ..^ lim lim
190 ax-resscn 9614 . . . . . . . . . . 11
191190a1i 11 . . . . . . . . . 10
192177, 191fssd 5750 . . . . . . . . 9
1931923ad2ant1 1051 . . . . . . . 8 ..^
194 inss2 3644 . . . . . . . . 9
195194a1i 11 . . . . . . . 8 ..^
196193, 195fssresd 5762 . . . . . . 7 ..^
197 mnfxr 11437 . . . . . . . . . 10
198197a1i 11 . . . . . . . . . . 11 ..^
19925adantr 472 . . . . . . . . . . . . 13 ..^
200 elfzofz 11962 . . . . . . . . . . . . . 14 ..^
201200adantl 473 . . . . . . . . . . . . 13 ..^
202199, 201ffvelrnd 6038 . . . . . . . . . . . 12 ..^
203202rexrd 9708 . . . . . . . . . . 11 ..^
204202mnfltd 11449 . . . . . . . . . . 11 ..^
205198, 203, 204xrltled 37574 . . . . . . . . . 10 ..^
206 iooss1 11696 . . . . . . . . . 10
207197, 205, 206sylancr 676 . . . . . . . . 9 ..^
2082073adant3 1050 . . . . . . . 8 ..^
209 fzofzp1 12037 . . . . . . . . . . . . . 14 ..^
210209adantl 473 . . . . . . . . . . . . 13 ..^
211199, 210ffvelrnd 6038 . . . . . . . . . . . 12 ..^
2122113adant3 1050 . . . . . . . . . . 11 ..^
213212rexrd 9708 . . . . . . . . . 10 ..^
2142023adant3 1050 . . . . . . . . . . . 12 ..^
215214rexrd 9708 . . . . . . . . . . 11 ..^
216 simp3 1032 . . . . . . . . . . 11 ..^
217 iocleub 37696 . . . . . . . . . . 11
218215, 213, 216, 217syl3anc 1292 . . . . . . . . . 10 ..^
219 iooss2 11697 . . . . . . . . . 10
220213, 218, 219syl2anc 673 . . . . . . . . 9 ..^
221 fourierdlem49.cn . . . . . . . . . . . . 13 ..^
222 cncff 22003 . . . . . . . . . . . . 13
223 fdm 5745 . . . . . . . . . . . . 13
224221, 222, 2233syl 18 . . . . . . . . . . . 12 ..^
225 ssdmres 5132 . . . . . . . . . . . 12
226224, 225sylibr 217 . . . . . . . . . . 11 ..^
227184adantr 472 . . . . . . . . . . 11 ..^
228226, 227sseqtrd 3454 . . . . . . . . . 10 ..^
2292283adant3 1050 . . . . . . . . 9 ..^
230220, 229sstrd 3428 . . . . . . . 8 ..^
231208, 230ssind 3647 . . . . . . 7 ..^
232 fourierdlem49.d . . . . . . . . . 10
233232, 191sstrd 3428 . . . . . . . . 9
2342333ad2ant1 1051 . . . . . . . 8 ..^
235194, 234syl5ss 3429 . . . . . . 7 ..^
236 eqid 2471 . . . . . . 7 fld fld
237 eqid 2471 . . . . . . 7 fldt fldt
2381363ad2ant1 1051 . . . . . . . . . 10 ..^
239238rexrd 9708 . . . . . . . . 9 ..^
240 iocgtlb 37695 . . . . . . . . . 10
241215, 213, 216, 240syl3anc 1292 . . . . . . . . 9 ..^
242238leidd 10201 . . . . . . . . 9 ..^
243215, 239, 239, 241, 242eliocd 37701 . . . . . . . 8 ..^
244 snunioo2 37702 . . . . . . . . . . 11
245215, 239, 241, 244syl3anc 1292 . . . . . . . . . 10 ..^
246245fveq2d 5883 . . . . . . . . 9 ..^ fldt fldt
247236cnfldtop 21882 . . . . . . . . . . 11 fld
248 ovex 6336 . . . . . . . . . . . . 13
249248inex1 4537 . . . . . . . . . . . 12
250 snex 4641 . . . . . . . . . . . 12
251249, 250unex 6608 . . . . . . . . . . 11
252 resttop 20253 . . . . . . . . . . 11 fld fldt
253247, 251, 252mp2an 686 . . . . . . . . . 10 fldt
254 retop 21860 . . . . . . . . . . . . 13
255254a1i 11 . . . . . . . . . . . 12 ..^
256251a1i 11 . . . . . . . . . . . 12 ..^
257 iooretop 21864 . . . . . . . . . . . . 13
258257a1i 11 . . . . . . . . . . . 12 ..^
259 elrestr 15405 . . . . . . . . . . . 12 t
260255, 256, 258, 259syl3anc 1292 . . . . . . . . . . 11 ..^ t
261 simpr 468 . . . . . . . . . . . . . . . 16 ..^
262 pnfxr 11435 . . . . . . . . . . . . . . . . . . . 20
263262a1i 11 . . . . . . . . . . . . . . . . . . 19 ..^
264238ltpnfd 11446 . . . . . . . . . . . . . . . . . . 19 ..^
265215, 263, 238, 241, 264eliood 37691 . . . . . . . . . . . . . . . . . 18 ..^
266 snidg 3986 . . . . . . . . . . . . . . . . . . . . 21
267 elun2 3593 . . . . . . . . . . . . . . . . . . . . 21
268266, 267syl 17 . . . . . . . . . . . . . . . . . . . 20
269136, 268syl 17 . . . . . . . . . . . . . . . . . . 19
2702693ad2ant1 1051 . . . . . . . . . . . . . . . . . 18 ..^
271265, 270elind 3609 . . . . . . . . . . . . . . . . 17 ..^
272271adantr 472 . . . . . . . . . . . . . . . 16 ..^
273261, 272eqeltrd 2549 . . . . . . . . . . . . . . 15 ..^
274273adantlr 729 . . . . . . . . . . . . . 14 ..^
275215adantr 472 . . . . . . . . . . . . . . . . 17 ..^
276262a1i 11 . . . . . . . . . . . . . . . . 17 ..^
277203adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
278136adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ..^
279278adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
280 iocssre 11739 . . . . . . . . . . . . . . . . . . . 20
281277, 279, 280syl2anc 673 . . . . . . . . . . . . . . . . . . 19 ..^
282 simpr 468 . . . . . . . . . . . . . . . . . . 19 ..^
283281, 282sseldd 3419 . . . . . . . . . . . . . . . . . 18 ..^
2842833adantl3 1188 . . . . . . . . . . . . . . . . 17 ..^
285279rexrd 9708 . . . . . . . . . . . . . . . . . . 19 ..^
286 iocgtlb 37695 . . . . . . . . . . . . . . . . . . 19
287277, 285, 282, 286syl3anc 1292 . . . . . . . . . . . . . . . . . 18 ..^
2882873adantl3 1188 . . . . . . . . . . . . . . . . 17 ..^
289284ltpnfd 11446 . . . . . . . . . . . . . . . . 17 ..^
290275, 276, 284, 288, 289eliood 37691 . . . . . . . . . . . . . . . 16 ..^
291290adantr 472 . . . . . . . . . . . . . . 15 ..^
292197a1i 11 . . . . . . . . . . . . . . . . . . 19 ..^
293285adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
294283adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
295294mnfltd 11449 . . . . . . . . . . . . . . . . . . 19 ..^
296136ad3antrrr 744 . . . . . . . . . . . . . . . . . . . 20 ..^
297 iocleub 37696 . . . . . . . . . . . . . . . . . . . . . 22
298277, 285, 282, 297syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21 ..^
299298adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
300 neqne 2651 . . . . . . . . . . . . . . . . . . . . . 22
301300necomd 2698 . . . . . . . . . . . . . . . . . . . . 21
302301adantl 473 . . . . . . . . . . . . . . . . . . . 20 ..^
303294, 296, 299, 302leneltd 9806 . . . . . . . . . . . . . . . . . . 19 ..^
304292, 293, 294, 295, 303eliood 37691 . . . . . . . . . . . . . . . . . 18 ..^
3053043adantll3 37428 . . . . . . . . . . . . . . . . 17 ..^
306229ad2antrr 740 . . . . . . . . . . . . . . . . . 18 ..^
307275adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
308213ad2antrr 740 . . . . . . . . . . . . . . . . . . 19 ..^
309284adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
310288adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
311238ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20 ..^
312212ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20 ..^
3133033adantll3 37428 . . . . . . . . . . . . . . . . . . . 20 ..^
314218ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20 ..^
315309, 311, 312, 313, 314ltletrd 9812 . . . . . . . . . . . . . . . . . . 19 ..^
316307, 308, 309, 310, 315eliood 37691 . . . . . . . . . . . . . . . . . 18 ..^
317306, 316sseldd 3419 . . . . . . . . . . . . . . . . 17 ..^
318305, 317elind 3609 . . . . . . . . . . . . . . . 16 ..^
319 elun1 3592 . . . . . . . . . . . . . . . 16
320318, 319syl 17 . . . . . . . . . . . . . . 15 ..^
321291, 320elind 3609 . . . . . . . . . . . . . 14 ..^
322274, 321pm2.61dan 808 . . . . . . . . . . . . 13 ..^
323215adantr 472 . . . . . . . . . . . . . 14 ..^
324239adantr 472 . . . . . . . . . . . . . 14 ..^
325 elinel1 3610 . . . . . . . . . . . . . . . 16
326 elioore 11691 . . . . . . . . . . . . . . . . 17
327326rexrd 9708 . . . . . . . . . . . . . . . 16
328325, 327syl 17 . . . . . . . . . . . . . . 15
329328adantl 473 . . . . . . . . . . . . . 14 ..^
330203adantr 472 . . . . . . . . . . . . . . . 16 ..^
331262a1i 11 . . . . . . . . . . . . . . . 16 ..^
332325adantl 473 . . . . . . . . . . . . . . . 16 ..^
333 ioogtlb 37688 . . . . . . . . . . . . . . . 16
334330, 331, 332, 333syl3anc 1292 . . . . . . . . . . . . . . 15 ..^
3353343adantl3 1188 . . . . . . . . . . . . . 14 ..^
336 elinel2 3611 . . . . . . . . . . . . . . . 16
337 elsni 3985 . . . . . . . . . . . . . . . . . . . . 21
338337adantl 473 . . . . . . . . . . . . . . . . . . . 20
339137adantr 472 . . . . . . . . . . . . . . . . . . . 20
340338, 339eqbrtrd 4416 . . . . . . . . . . . . . . . . . . 19
341340adantlr 729 . . . . . . . . . . . . . . . . . 18
342 simpll 768 . . . . . . . . . . . . . . . . . . 19
343 elunnel2 37423 . . . . . . . . . . . . . . . . . . . 20
344343adantll 728 . . . . . . . . . . . . . . . . . . 19
345 elinel1 3610 . . . . . . . . . . . . . . . . . . . 20
346 elioore 11691 . . . . . . . . . . . . . . . . . . . . . 22
347346adantl 473 . . . . . . . . . . . . . . . . . . . . 21
348136adantr 472 . . . . . . . . . . . . . . . . . . . . 21
349197a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
350348rexrd 9708 . . . . . . . . . . . . . . . . . . . . . 22
351 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22
352 iooltub 37706 . . . . . . . . . . . . . . . . . . . . . 22
353349, 350, 351, 352syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21
354347, 348, 353ltled 9800 . . . . . . . . . . . . . . . . . . . 20
355345, 354sylan2 482 . . . . . . . . . . . . . . . . . . 19
356342, 344, 355syl2anc 673 . . . . . . . . . . . . . . . . . 18
357341, 356pm2.61dan 808 . . . . . . . . . . . . . . . . 17
358357adantlr 729 . . . . . . . . . . . . . . . 16 ..^
359336, 358sylan2 482 . . . . . . . . . . . . . . 15 ..^
3603593adantl3 1188 . . . . . . . . . . . . . 14 ..^
361323, 324, 329, 335, 360eliocd 37701 . . . . . . . . . . . . 13 ..^
362322, 361impbida 850 . . . . . . . . . . . 12 ..^
363362eqrdv 2469 . . . . . . . . . . 11 ..^