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

Theorem fouriersw 31903
 Description: Fourier series convergence, for the square wave function. Where is discontinuous, the series converges to , the average value of the left and the right limits. Notice that is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fouriersw.t
fouriersw.f
fouriersw.x
fouriersw.z
fouriersw.y
Assertion
Ref Expression
fouriersw
Distinct variable groups:   ,,   ,   ,,   ,   ,
Allowed substitution hints:   (,,)   (,)   ()   (,)

Proof of Theorem fouriersw
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nnuz 11126 . . . . . . 7
2 1zzd 10902 . . . . . . 7
3 eqidd 2444 . . . . . . . . 9
4 oveq2 6289 . . . . . . . . . . . . . 14
54oveq1d 6296 . . . . . . . . . . . . 13
65oveq1d 6296 . . . . . . . . . . . 12
76fveq2d 5860 . . . . . . . . . . 11
87, 5oveq12d 6299 . . . . . . . . . 10
98adantl 466 . . . . . . . . 9
10 id 22 . . . . . . . . 9
11 ovex 6309 . . . . . . . . . 10
1211a1i 11 . . . . . . . . 9
133, 9, 10, 12fvmptd 5946 . . . . . . . 8
1413adantl 466 . . . . . . 7
15 2z 10903 . . . . . . . . . . . . . . 15
1615a1i 11 . . . . . . . . . . . . . 14
17 nnz 10893 . . . . . . . . . . . . . 14
1816, 17zmulcld 10981 . . . . . . . . . . . . 13
19 1zzd 10902 . . . . . . . . . . . . 13
2018, 19zsubcld 10980 . . . . . . . . . . . 12
2120zcnd 10976 . . . . . . . . . . 11
22 fouriersw.x . . . . . . . . . . . . 13
2322recni 9611 . . . . . . . . . . . 12
2423a1i 11 . . . . . . . . . . 11
2521, 24mulcld 9619 . . . . . . . . . 10
2625sincld 13846 . . . . . . . . 9
27 0red 9600 . . . . . . . . . 10
28 2re 10612 . . . . . . . . . . . . . 14
2928a1i 11 . . . . . . . . . . . . 13
30 1red 9614 . . . . . . . . . . . . 13
3129, 30remulcld 9627 . . . . . . . . . . . 12
3231, 30resubcld 9994 . . . . . . . . . . 11
3320zred 10975 . . . . . . . . . . 11
34 0lt1 10082 . . . . . . . . . . . . 13
35 2t1e2 10691 . . . . . . . . . . . . . . 15
3635oveq1i 6291 . . . . . . . . . . . . . 14
37 2m1e1 10657 . . . . . . . . . . . . . 14
3836, 37eqtr2i 2473 . . . . . . . . . . . . 13
3934, 38breqtri 4460 . . . . . . . . . . . 12
4039a1i 11 . . . . . . . . . . 11
4118zred 10975 . . . . . . . . . . . 12
42 nnre 10550 . . . . . . . . . . . . 13
43 0le2 10633 . . . . . . . . . . . . . 14
4443a1i 11 . . . . . . . . . . . . 13
45 nnge1 10569 . . . . . . . . . . . . 13
4630, 42, 29, 44, 45lemul2ad 10493 . . . . . . . . . . . 12
4731, 41, 30, 46lesub1dd 10175 . . . . . . . . . . 11
4827, 32, 33, 40, 47ltletrd 9745 . . . . . . . . . 10
4927, 48gtned 9723 . . . . . . . . 9
5026, 21, 49divcld 10327 . . . . . . . 8
5150adantl 466 . . . . . . 7
52 picn 22828 . . . . . . . . . . 11
5352a1i 11 . . . . . . . . . 10
54 4cn 10620 . . . . . . . . . . 11
5554a1i 11 . . . . . . . . . 10
56 4ne0 10639 . . . . . . . . . . 11
5756a1i 11 . . . . . . . . . 10
5853, 55, 57divcld 10327 . . . . . . . . 9
59 eqid 2443 . . . . . . . . . . . . . . . 16
60 0cnd 9592 . . . . . . . . . . . . . . . . 17
6154a1i 11 . . . . . . . . . . . . . . . . . . 19
62 nncn 10551 . . . . . . . . . . . . . . . . . . . 20
63 mulcl 9579 . . . . . . . . . . . . . . . . . . . 20
6462, 52, 63sylancl 662 . . . . . . . . . . . . . . . . . . 19
6552a1i 11 . . . . . . . . . . . . . . . . . . . 20
66 nnne0 10575 . . . . . . . . . . . . . . . . . . . 20
67 0re 9599 . . . . . . . . . . . . . . . . . . . . . 22
68 pipos 22829 . . . . . . . . . . . . . . . . . . . . . 22
6967, 68gtneii 9699 . . . . . . . . . . . . . . . . . . . . 21
7069a1i 11 . . . . . . . . . . . . . . . . . . . 20
7162, 65, 66, 70mulne0d 10208 . . . . . . . . . . . . . . . . . . 19
7261, 64, 71divcld 10327 . . . . . . . . . . . . . . . . . 18
7323a1i 11 . . . . . . . . . . . . . . . . . . . 20
7462, 73mulcld 9619 . . . . . . . . . . . . . . . . . . 19
7574sincld 13846 . . . . . . . . . . . . . . . . . 18
7672, 75mulcld 9619 . . . . . . . . . . . . . . . . 17
7760, 76ifcld 3969 . . . . . . . . . . . . . . . 16
7859, 77fmpti 6039 . . . . . . . . . . . . . . 15
7978a1i 11 . . . . . . . . . . . . . 14
80 eqidd 2444 . . . . . . . . . . . . . . . . . 18
81 breq2 4441 . . . . . . . . . . . . . . . . . . . 20
82 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22
8382oveq2d 6297 . . . . . . . . . . . . . . . . . . . . 21
84 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22
8584fveq2d 5860 . . . . . . . . . . . . . . . . . . . . 21
8683, 85oveq12d 6299 . . . . . . . . . . . . . . . . . . . 20
8781, 86ifbieq2d 3951 . . . . . . . . . . . . . . . . . . 19
8887adantl 466 . . . . . . . . . . . . . . . . . 18
89 c0ex 9593 . . . . . . . . . . . . . . . . . . . 20
90 ovex 6309 . . . . . . . . . . . . . . . . . . . 20
9189, 90ifex 3995 . . . . . . . . . . . . . . . . . . 19
9291a1i 11 . . . . . . . . . . . . . . . . . 18
9380, 88, 10, 92fvmptd 5946 . . . . . . . . . . . . . . . . 17
9493adantr 465 . . . . . . . . . . . . . . . 16
95 simpr 461 . . . . . . . . . . . . . . . . . 18
96 simpl 457 . . . . . . . . . . . . . . . . . . 19
97 2nn 10700 . . . . . . . . . . . . . . . . . . 19
98 nndivdvds 13973 . . . . . . . . . . . . . . . . . . 19
9996, 97, 98sylancl 662 . . . . . . . . . . . . . . . . . 18
10095, 99mpbird 232 . . . . . . . . . . . . . . . . 17
101100iftrued 3934 . . . . . . . . . . . . . . . 16
10294, 101eqtrd 2484 . . . . . . . . . . . . . . 15
1031023adant1 1015 . . . . . . . . . . . . . 14
104 fouriersw.f . . . . . . . . . . . . . . . . . 18
105 1re 9598 . . . . . . . . . . . . . . . . . . . 20
106105renegcli 9885 . . . . . . . . . . . . . . . . . . . 20
107105, 106keepel 3994 . . . . . . . . . . . . . . . . . . 19
108107a1i 11 . . . . . . . . . . . . . . . . . 18
109104, 108fmpti 6039 . . . . . . . . . . . . . . . . 17
110 fouriersw.t . . . . . . . . . . . . . . . . 17
111 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . 24
112111breq1d 4447 . . . . . . . . . . . . . . . . . . . . . . 23
113112ifbid 3948 . . . . . . . . . . . . . . . . . . . . . 22
114113cbvmptv 4528 . . . . . . . . . . . . . . . . . . . . 21
115104, 114eqtri 2472 . . . . . . . . . . . . . . . . . . . 20
116115a1i 11 . . . . . . . . . . . . . . . . . . 19
117 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . 24
118 pire 22827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
11928, 118remulcli 9613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120110, 119eqeltri 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121120recni 9611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122121mulid2i 9602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
123122eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . 26
124123oveq2i 6292 . . . . . . . . . . . . . . . . . . . . . . . . 25
125124oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . 24
126117, 125syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . 23
127126adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
128 simpl 457 . . . . . . . . . . . . . . . . . . . . . . 23
129 2pos 10634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
13028, 118, 129, 68mulgt0ii 9721 . . . . . . . . . . . . . . . . . . . . . . . . . 26
131110eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . 26
132130, 131breqtri 4460 . . . . . . . . . . . . . . . . . . . . . . . . 25
133120, 132elrpii 11233 . . . . . . . . . . . . . . . . . . . . . . . 24
134133a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
135 1zzd 10902 . . . . . . . . . . . . . . . . . . . . . . 23
136 modcyc 12012 . . . . . . . . . . . . . . . . . . . . . . 23
137128, 134, 135, 136syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . 22
138127, 137eqtrd 2484 . . . . . . . . . . . . . . . . . . . . 21
139138breq1d 4447 . . . . . . . . . . . . . . . . . . . 20
140139ifbid 3948 . . . . . . . . . . . . . . . . . . 19
141 id 22 . . . . . . . . . . . . . . . . . . . 20
142120a1i 11 . . . . . . . . . . . . . . . . . . . 20
143141, 142readdcld 9626 . . . . . . . . . . . . . . . . . . 19
144116, 140, 143, 108fvmptd 5946 . . . . . . . . . . . . . . . . . 18
145104fvmpt2 5948 . . . . . . . . . . . . . . . . . . 19
146107, 145mpan2 671 . . . . . . . . . . . . . . . . . 18
147144, 146eqtr4d 2487 . . . . . . . . . . . . . . . . 17
148 eqid 2443 . . . . . . . . . . . . . . . . 17
149 snfi 7598 . . . . . . . . . . . . . . . . . 18
150 eldifi 3611 . . . . . . . . . . . . . . . . . . . . . 22
151 0xr 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
153118rexri 9649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
155 elioore 11569 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
156155adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
157 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
158118renegcli 9885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159158rexri 9649 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160 iooltub 31484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
161159, 153, 160mp3an12 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
162161adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
163152, 154, 156, 157, 162eliood 31467 . . . . . . . . . . . . . . . . . . . . . . . . 25
164 negpilt0 31411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165158, 67, 164ltleii 9710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166 iooss1 11574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
167159, 165, 166mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168167sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
169104reseq1i 5259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170 ioossre 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171 resmpt 5313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172170, 171ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173 elioore 11569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175 0red 9600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176 ioogtlb 31464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
177151, 153, 176mp3an12 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178175, 173, 177ltled 9736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181168, 161syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182 pirp 22830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183 2timesgt 31424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185184, 131breqtri 4460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187173, 179, 180, 181, 186lttrd 9746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188 modid 12001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
189173, 174, 178, 187, 188syl22anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190189, 181eqbrtrd 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191190iftrued 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192191mpteq2ia 4519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193169, 172, 1923eqtrri 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194193oveq2i 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195 reelprrecn 9587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196195a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197 iooretop 21250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 fld fld
199198tgioo2 21285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 fldt
200197, 199eleqtri 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 fldt
201200a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 fldt
202 1cnd 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203196, 201, 202dvmptconst 31614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204203trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205 ssid 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206 ax-resscn 9552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207 fss 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
208109, 206, 207mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209 dvresioo 31622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
210205, 208, 209mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211194, 204, 2103eqtr3i 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212211dmeqi 5194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
21489, 213dmmpti 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215212, 214eqtr3i 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216 ssdmres 5285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217215, 216mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218217sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
219168, 218elind 3673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
220 dmres 5284 . . . . . . . . . . . . . . . . . . . . . . . . . 26
221219, 220syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . 25
222163, 221syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
223222adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23
224159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
225151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
226155ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
227 ioogtlb 31464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
228159, 153, 227mp3an12 1315 . . . . . . . . . . . . . . . . . . . . . . . . . 26
229228ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
230 0red 9600 . . . . . . . . . . . . . . . . . . . . . . . . . 26
231 neqne 31388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
232231ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26
233 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
234226, 230, 232, 233lttri5d 31448 . . . . . . . . . . . . . . . . . . . . . . . . 25
235224, 225, 226, 229, 234eliood 31467 . . . . . . . . . . . . . . . . . . . . . . . 24
23667, 118, 68ltleii 9710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237 iooss2 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
238153, 236, 237mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
239238sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . 26
240104reseq1i 5259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241 ioossre 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242 resmpt 5313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243241, 242ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245 elioore 11569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247245, 246modcld 11983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248245, 143syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249522timesi 10663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250110, 249eqtri 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251250oveq2i 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252 negpicn 22831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253252, 52, 52addassi 9607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254253eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
25552negidi 9893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
25652, 252, 255addcomli 9775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257256oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
25852addid2i 9771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259257, 258eqtri 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260251, 254, 2593eqtrri 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
261260a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
262158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
263120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
264239, 228syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
265262, 245, 263, 264ltadd1dd 10170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266261, 265eqbrtrd 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267244, 248, 266ltled 9736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268 0red 9600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269158, 120readdcli 9612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
27168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272271, 260syl6breq 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273268, 270, 248, 272, 265lttrd 9746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274268, 248, 273ltled 9736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275245recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277275, 276addcomd 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278 iooltub 31484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
279159, 151, 278mp3an12 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280 ltaddneg 31433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
281245, 120, 280sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282279, 281mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283277, 282eqbrtrd 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284274, 283jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
285 modid2 12004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
286248, 133, 285sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
287284, 286mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
289133a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
290 1zzd 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291141, 289, 290, 136syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292288, 291eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293245, 292syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294287, 293eqtr3d 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295267, 294breqtrd 4461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296244, 247, 295leimnltd 31421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297296iffalsed 3937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298297mpteq2ia 4519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299240, 243, 2983eqtrri 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300299oveq2i 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301 iooretop 21250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302301, 199eleqtri 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 fldt
303302a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 fldt
304202negcld 9923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305196, 303, 304dvmptconst 31614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306305trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307 dvresioo 31622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
308205, 208, 307mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309300, 306, 3083eqtr3i 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310309dmeqi 5194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
31289, 311dmmpti 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313310, 312eqtr3i 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314 ssdmres 5285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315313, 314mpbir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
316315sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . 26
317239, 316elind 3673 . . . . . . . . . . . . . . . . . . . . . . . . 25
318317, 220syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . 24
319235, 318syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
320223, 319pm2.61dan 791 . . . . . . . . . . . . . . . . . . . . . 22
321150, 320sylan 471 . . . . . . . . . . . . . . . . . . . . 21
322 eldifn 3612 . . . . . . . . . . . . . . . . . . . . . 22
323322adantr 465 . . . . . . . . . . . . . . . . . . . . 21
324321, 323condan 794 . . . . . . . . . . . . . . . . . . . 20
325 elsn 4028 . . . . . . . . . . . . . . . . . . . 20
326324, 325sylibr 212 . . . . . . . . . . . . . . . . . . 19
327326ssriv 3493 . . . . . . . . . . . . . . . . . 18
328 ssfi 7742 . . . . . . . . . . . . . . . . . 18
329149, 327, 328mp2an 672 . . . . . . . . . . . . . . . . 17
330 inss1 3703 . . . . . . . . . . . . . . . . . . . . . 22
331220, 330eqsstri 3519 . . . . . . . . . . . . . . . . . . . . 21
332 ioosscn 31463 . . . . . . . . . . . . . . . . . . . . 21
333331, 332sstri 3498 . . . . . . . . . . . . . . . . . . . 20
334333a1i 11 . . . . . . . . . . . . . . . . . . 19
335 dvf 22288 . . . . . . . . . . . . . . . . . . . . . 22
336 fresin 5744 . . . . . . . . . . . . . . . . . . . . . 22
337 ffdm 5735 . . . . . . . . . . . . . . . . . . . . . 22
338335, 336, 337mp2b 10 . . . . . . . . . . . . . . . . . . . . 21
339338simpli 458 . . . . . . . . . . . . . . . . . . . 20
340339a1i 11 . . . . . . . . . . . . . . . . . . 19
341159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
342151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
343 ioossre 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
344331sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
345343, 344sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . . . 26
346345adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
347344, 228syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
348347adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
349 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25
350341, 342, 346, 348, 349eliood 31467 . . . . . . . . . . . . . . . . . . . . . . . 24
351 elun1 3656 . . . . . . . . . . . . . . . . . . . . . . . 24
352350, 351syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
353 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . 24
354 0red 9600 . . . . . . . . . . . . . . . . . . . . . . . . 25
355345adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
356 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
357354, 355, 356nltled 31426 . . . . . . . . . . . . . . . . . . . . . . . . 25
358 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361208a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362 0red 9600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363 mnfxr 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364363a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365362mnfltd 31440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366360, 364, 362, 365lptioo2 31545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367 incom 3676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368 ioossre 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369 df-ss 3475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370368, 369mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371367, 370eqtr2i 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372371fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373366, 372syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374 pnfxr 11331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375374a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376362ltpnfd 31429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377360, 362, 375, 376lptioo1 31546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378 incom 3676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379 ioossre 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380 df-ss 3475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381379, 380mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382378, 381eqtr2i 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383382fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384377, 383syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386 mnfle 11352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387159, 386ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388 iooss1 11574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
389363, 387, 388mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390389a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391 ioosscn 31463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392390, 391syl6ss 3501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393 0cnd 9592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394385, 392, 304, 393constlimc 31538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395 resabs1 5292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396389, 395ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397299, 396eqtr4i 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398397oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399 fssres 5741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
400208, 368, 399mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401400a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402391a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 fldt fldt
404 0le0 10632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405 elioc2 11597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
406159, 67, 405mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
40767, 164, 404, 406mpbir3an 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408198cnfldtop 21268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 fld
409 ovex 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410 resttop 19638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 fld fldt
411408, 409, 410mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt
412159a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 t t
414387a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415364, 412, 362, 360, 413, 414, 362iocopn 31496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 t
416415trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 t
417199oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 t fldt t
418 iocssre 11614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
419363, 67, 418mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420195elexi 3105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421 restabs 19643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 fld fldt t fldt
422408, 419, 420, 421mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 fldt t fldt
423417, 422eqtri 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 t fldt
424416, 423eleqtri 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt
425 isopn3i 19560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt fldt fldt
426411, 424, 425mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 fldt
427 mnflt0 11344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428 snunioo2 31480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
429363, 151, 427, 428mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430429eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431430oveq2i 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 fldt fldt
432431fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt fldt
433 snunioo2 31480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
434159, 151, 164, 433mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435434eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436432, 435fveq12i 5861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 fldt fldt
437426, 436eqtr3i 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 fldt
438407, 437eleqtri 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 fldt
439438a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 fldt
440401, 390, 402, 198, 403, 439limcres 22267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441440trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442398, 441eqtri 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443394, 442syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445 ioosscn 31463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446445a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447444, 446, 202, 393constlimc 31538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448 ltpnf 11341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449 xrltle 11365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
450153, 374, 449mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451118, 448, 450mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452 iooss2 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
453374, 451, 452mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454 resabs1 5292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455453, 454ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456193, 455eqtr4i 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457456oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458 fssres 5741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
459208, 379, 458mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460459a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461453a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462 ioosscn 31463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463462a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 fldt fldt
465 elico2 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
46667, 153, 465mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
46767, 404, 68, 466mpbir3an 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468 ovex 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469 resttop 19638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 fld fldt
470408, 468, 469mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt
471153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 t t
473451a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474362, 471, 375, 360, 472, 473icoopn 31501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 t
475474trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 t
476199oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 t fldt t
477 rge0ssre 11638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478 restabs 19643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 fld fldt t fldt
479408, 477, 420, 478mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 fldt t fldt
480476, 479eqtri 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 t fldt
481475, 480eleqtri 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt
482 isopn3i 19560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt fldt fldt
483470, 481, 482mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 fldt
484 0ltpnf 11342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485 snunioo1 31488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
486151, 374, 484, 485mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487486eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488487oveq2i 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 fldt fldt
489488fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 fldt fldt
490 snunioo1 31488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
491151, 153, 68, 490mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492491eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493489, 492fveq12i 5861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 fldt fldt
494483, 493eqtr3i 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 fldt
495467, 494eleqtri 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 fldt
496495a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 fldt
497460, 461, 463, 198, 464, 496limcres 22267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498497trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499457, 498eqtri 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500447, 499syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501 neg1lt0 10649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502106, 67, 105lttri 9713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
503501, 34, 502mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504106, 503ltneii 9700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505504a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506198, 359, 360, 361, 362, 373, 384, 443, 500, 505jumpncnp 31608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 fld
507506trud 1392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 fld
508206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
509208a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
510205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
511 inss2 3704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512220, 511eqsstri 3519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513512sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514199, 198dvcnp2 22300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 fld
515508, 509, 510, 513, 514syl31anc 1232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 fld
516507, 515mto 176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
517516a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
518358, 517eqneltrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
519518necon2ai 2678 . . . . . . . . . . . . . . . . . . . . . . . . . 26
520519adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
521354, 355, 357, 520leneltd 31443 . . . . . . . . . . . . . . . . . . . . . . . 24
522344, 163sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . 25
523 elun2 3657 . . . . . . . . . . . . . . . . . . . . . . . . 25
524522, 523syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
525353, 521, 524syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
526352, 525pm2.61dan 791 . . . . . . . . . . . . . . . . . . . . . 22
527 ovex 6309 . . . . . . . . . . . . . . . . . . . . . . 23
528 ovex 6309 . . . . . . . . . . . . . . . . . . . . . . 23
529527, 528unipr 4247 . . . . . . . . . . . . . . . . . . . . . 22
530526, 529syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . 21
531530ssriv 3493 . . . . . . . . . . . . . . . . . . . 20
532531a1i 11 . . . . . . . . . . . . . . . . . . 19
533 ineq2 3679 . . . . . . . . . . . . . . . . . . . . . . 23
534 retop 21245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
535 ovex 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536535resex 5307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537536dmex 6718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
538534, 537pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . . . . . 26
539318ssriv 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
540 ssid 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
541301, 539, 5403pm3.2i 1175 . . . . . . . . . . . . . . . . . . . . . . . . . 26
542 restopnb 19653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 t
543538, 541, 542mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . 25 t
544301, 543mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . 24 t
545 inss2 3704 . . . . . . . . . . . . . . . . . . . . . . . . 25
546539, 540ssini 3706 . . . . . . . . . . . . . . . . . . . . . . . . 25
547545, 546eqssi 3505 . . . . . . . . . . . . . . . . . . . . . . . 24
548199oveq1i 6291 . . . . . . . . . . . . . . . . . . . . . . . . 25 t fldt t
549331, 343sstri 3498 . . . . . . . . . . . . . . . . . . . . . . . . . 26
550 restabs 19643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld fldt t fldt
551408, 549, 420, 550mp3an 1325 . . . . . . . . . . . . . . . . . . . . . . . . 25 fldt t fldt
552548, 551eqtr2i 2473 . . . . . . . . . . . . . . . . . . . . . . . 24 fldt t
553544, 547, 5523eltr4i 2544 . . . . . . . . . . . . . . . . . . . . . . 23 fldt
554533, 553syl6eqel 2539 . . . . . . . . . . . . . . . . . . . . . 22 fldt
555554adantl 466 . . . . . . . . . . . . . . . . . . . . 21 fldt
556 neqne 31388 . . . . . . . . . . . . . . . . . . . . . . 23
557 elprn1 31547 . . . . . . . . . . . . . . . . . . . . . . 23
558556, 557sylan2 474 . . . . . . . . . . . . . . . . . . . . . 22
559 ineq2 3679 . . . . . . . . . . . . . . . . . . . . . . 23
560221ssriv 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
561 ssid 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
562197, 560, 5613pm3.2i 1175 . . . . . . . . . . . . . . . . . . . . . . . . . 26
563 restopnb 19653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 t
564538, 562, 563mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . 25 t
565197, 564mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . 24 t
566 inss2 3704 . . . . . . . . . . . . . . . . . . . . . . . . 25
567560, 561ssini 3706 . . . . . . . . . . . . . . . . . . . . . . . . 25
568566, 567eqssi 3505 . . . . . . . . . . . . . . . . . . . . . . . 24
569565, 568, 5523eltr4i 2544 . . . . . . . . . . . . . . . . . . . . . . 23 fldt
570559, 569syl6eqel 2539 . . . . . . . . . . . . . . . . . . . . . 22