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

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

Proof of Theorem fourierdlem48
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 464 . . 3
2 0zd 10973 . . . . . 6
3 fourierdlem48.m . . . . . . 7
43nnzd 11062 . . . . . 6
53nngt0d 10675 . . . . . 6
6 fzolb 11953 . . . . . 6 ..^
72, 4, 5, 6syl3anbrc 1214 . . . . 5 ..^
87adantr 472 . . . 4 ..^
9 fourierdlem48.b . . . . . . . . . 10
10 fourierdlem48.x . . . . . . . . . 10
119, 10resubcld 10068 . . . . . . . . 9
12 fourierdlem48.t . . . . . . . . . 10
13 fourierdlem48.a . . . . . . . . . . 11
149, 13resubcld 10068 . . . . . . . . . 10
1512, 14syl5eqel 2553 . . . . . . . . 9
16 fourierdlem48.altb . . . . . . . . . . . 12
1713, 9posdifd 10221 . . . . . . . . . . . 12
1816, 17mpbid 215 . . . . . . . . . . 11
1918, 12syl6breqr 4436 . . . . . . . . . 10
2019gt0ne0d 10199 . . . . . . . . 9
2111, 15, 20redivcld 10457 . . . . . . . 8
2221adantr 472 . . . . . . 7
2322flcld 12067 . . . . . 6
24 1zzd 10992 . . . . . 6
2523, 24zsubcld 11068 . . . . 5
26 id 22 . . . . . . . 8
2712a1i 11 . . . . . . . 8
2826, 27oveq12d 6326 . . . . . . 7
299recnd 9687 . . . . . . . 8
3013recnd 9687 . . . . . . . 8
3129, 30nncand 10010 . . . . . . 7
3228, 31sylan9eqr 2527 . . . . . 6
33 fourierdlem48.q . . . . . . . . . . . . . 14
34 fourierdlem48.p . . . . . . . . . . . . . . . 16 ..^
3534fourierdlem2 38083 . . . . . . . . . . . . . . 15 ..^
363, 35syl 17 . . . . . . . . . . . . . 14 ..^
3733, 36mpbid 215 . . . . . . . . . . . . 13 ..^
3837simpld 466 . . . . . . . . . . . 12
39 elmapi 7511 . . . . . . . . . . . 12
4038, 39syl 17 . . . . . . . . . . 11
413nnnn0d 10949 . . . . . . . . . . . . 13
42 nn0uz 11217 . . . . . . . . . . . . 13
4341, 42syl6eleq 2559 . . . . . . . . . . . 12
44 eluzfz1 11832 . . . . . . . . . . . 12
4543, 44syl 17 . . . . . . . . . . 11
4640, 45ffvelrnd 6038 . . . . . . . . . 10
4746rexrd 9708 . . . . . . . . 9
48 1zzd 10992 . . . . . . . . . . . . . 14
492, 4, 483jca 1210 . . . . . . . . . . . . 13
50 0le1 10158 . . . . . . . . . . . . . 14
5150a1i 11 . . . . . . . . . . . . 13
523nnge1d 10674 . . . . . . . . . . . . 13
5349, 51, 52jca32 544 . . . . . . . . . . . 12
54 elfz2 11817 . . . . . . . . . . . 12
5553, 54sylibr 217 . . . . . . . . . . 11
5640, 55ffvelrnd 6038 . . . . . . . . . 10
5756rexrd 9708 . . . . . . . . 9
5813rexrd 9708 . . . . . . . . 9
5937simprd 470 . . . . . . . . . . 11 ..^
6059simplld 769 . . . . . . . . . 10
6113leidd 10201 . . . . . . . . . 10
6260, 61eqbrtrd 4416 . . . . . . . . 9
6360eqcomd 2477 . . . . . . . . . 10
64 0re 9661 . . . . . . . . . . . . 13
65 eleq1 2537 . . . . . . . . . . . . . . . 16 ..^ ..^
6665anbi2d 718 . . . . . . . . . . . . . . 15 ..^ ..^
67 fveq2 5879 . . . . . . . . . . . . . . . 16
68 oveq1 6315 . . . . . . . . . . . . . . . . 17
6968fveq2d 5883 . . . . . . . . . . . . . . . 16
7067, 69breq12d 4408 . . . . . . . . . . . . . . 15
7166, 70imbi12d 327 . . . . . . . . . . . . . 14 ..^ ..^
7237simprrd 775 . . . . . . . . . . . . . . 15 ..^
7372r19.21bi 2776 . . . . . . . . . . . . . 14 ..^
7471, 73vtoclg 3093 . . . . . . . . . . . . 13 ..^
7564, 74ax-mp 5 . . . . . . . . . . . 12 ..^
767, 75mpdan 681 . . . . . . . . . . 11
77 1e0p1 11102 . . . . . . . . . . . 12
7877fveq2i 5882 . . . . . . . . . . 11
7976, 78syl6breqr 4436 . . . . . . . . . 10
8063, 79eqbrtrd 4416 . . . . . . . . 9
8147, 57, 58, 62, 80elicod 11710 . . . . . . . 8
8278oveq2i 6319 . . . . . . . 8
8381, 82syl6eleq 2559 . . . . . . 7
8483adantr 472 . . . . . 6
8532, 84eqeltrd 2549 . . . . 5
86 fourierdlem48.e . . . . . . . . . . 11
8786a1i 11 . . . . . . . . . 10
88 id 22 . . . . . . . . . . . 12
89 fveq2 5879 . . . . . . . . . . . 12
9088, 89oveq12d 6326 . . . . . . . . . . 11
9190adantl 473 . . . . . . . . . 10
92 fourierdlem48.z . . . . . . . . . . . . . 14
9392a1i 11 . . . . . . . . . . . . 13
94 oveq2 6316 . . . . . . . . . . . . . . . . 17
9594oveq1d 6323 . . . . . . . . . . . . . . . 16
9695fveq2d 5883 . . . . . . . . . . . . . . 15
9796oveq1d 6323 . . . . . . . . . . . . . 14
9897adantl 473 . . . . . . . . . . . . 13
9921flcld 12067 . . . . . . . . . . . . . . 15
10099zred 11063 . . . . . . . . . . . . . 14
101100, 15remulcld 9689 . . . . . . . . . . . . 13
10293, 98, 10, 101fvmptd 5969 . . . . . . . . . . . 12
103102, 101eqeltrd 2549 . . . . . . . . . . 11
10410, 103readdcld 9688 . . . . . . . . . 10
10587, 91, 10, 104fvmptd 5969 . . . . . . . . 9
106102oveq2d 6324 . . . . . . . . 9
107105, 106eqtrd 2505 . . . . . . . 8
108107oveq1d 6323 . . . . . . 7
10910recnd 9687 . . . . . . . 8
110101recnd 9687 . . . . . . . 8
11115recnd 9687 . . . . . . . 8
112109, 110, 111addsubassd 10025 . . . . . . 7
11399zcnd 11064 . . . . . . . . 9
114113, 111mulsubfacd 10099 . . . . . . . 8
115114oveq2d 6324 . . . . . . 7
116108, 112, 1153eqtrd 2509 . . . . . 6
117116adantr 472 . . . . 5
118 oveq1 6315 . . . . . . . . 9
119118oveq2d 6324 . . . . . . . 8
120119eqeq2d 2481 . . . . . . 7
121120anbi2d 718 . . . . . 6
122121rspcev 3136 . . . . 5
12325, 85, 117, 122syl12anc 1290 . . . 4
12467, 69oveq12d 6326 . . . . . . . 8
125124eleq2d 2534 . . . . . . 7
126125anbi1d 719 . . . . . 6
127126rexbidv 2892 . . . . 5
128127rspcev 3136 . . . 4 ..^ ..^
1298, 123, 128syl2anc 673 . . 3 ..^
130 ovex 6336 . . . 4
131 eleq1 2537 . . . . . . . 8
132 eqeq1 2475 . . . . . . . 8
133131, 132anbi12d 725 . . . . . . 7
1341332rexbidv 2897 . . . . . 6 ..^ ..^
135134anbi2d 718 . . . . 5 ..^ ..^
136135imbi1d 324 . . . 4 ..^ lim ..^ lim
137 simpr 468 . . . . 5 ..^ ..^
138 nfv 1769 . . . . . . 7
139 nfre1 2846 . . . . . . 7 ..^
140138, 139nfan 2031 . . . . . 6 ..^
141 nfv 1769 . . . . . . 7
142 nfcv 2612 . . . . . . . 8 ..^
143 nfre1 2846 . . . . . . . 8
144142, 143nfrex 2848 . . . . . . 7 ..^
145141, 144nfan 2031 . . . . . 6 ..^
146 simp1 1030 . . . . . . . . . 10 ..^
147 simp2l 1056 . . . . . . . . . 10 ..^ ..^
148 simp3l 1058 . . . . . . . . . 10 ..^
149146, 147, 148jca31 543 . . . . . . . . 9 ..^ ..^
150 simp2r 1057 . . . . . . . . 9 ..^
151 simp3r 1059 . . . . . . . . 9 ..^
152 fourierdlem48.ch . . . . . . . . . 10 ..^
153152biimpi 199 . . . . . . . . . . . . . . . . . 18 ..^
154153simplld 769 . . . . . . . . . . . . . . . . 17 ..^
155154simplld 769 . . . . . . . . . . . . . . . 16
156 fourierdlem48.f . . . . . . . . . . . . . . . 16
157 frel 5744 . . . . . . . . . . . . . . . 16
158155, 156, 1573syl 18 . . . . . . . . . . . . . . 15
159 resindm 5155 . . . . . . . . . . . . . . . 16
160159eqcomd 2477 . . . . . . . . . . . . . . 15
161158, 160syl 17 . . . . . . . . . . . . . 14
162 fdm 5745 . . . . . . . . . . . . . . . . 17
163155, 156, 1623syl 18 . . . . . . . . . . . . . . . 16
164163ineq2d 3625 . . . . . . . . . . . . . . 15
165164reseq2d 5111 . . . . . . . . . . . . . 14
166161, 165eqtrd 2505 . . . . . . . . . . . . 13
167166oveq1d 6323 . . . . . . . . . . . 12 lim lim
168155, 156syl 17 . . . . . . . . . . . . . . 15
169 ax-resscn 9614 . . . . . . . . . . . . . . . 16
170169a1i 11 . . . . . . . . . . . . . . 15
171168, 170fssd 5750 . . . . . . . . . . . . . 14
172 inss2 3644 . . . . . . . . . . . . . . 15
173172a1i 11 . . . . . . . . . . . . . 14
174171, 173fssresd 5762 . . . . . . . . . . . . 13
175 pnfxr 11435 . . . . . . . . . . . . . . . 16
176175a1i 11 . . . . . . . . . . . . . . 15
177154simplrd 771 . . . . . . . . . . . . . . . . . . 19 ..^
17840adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
179 fzofzp1 12037 . . . . . . . . . . . . . . . . . . . . 21 ..^
180179adantl 473 . . . . . . . . . . . . . . . . . . . 20 ..^
181178, 180ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19 ..^
182155, 177, 181syl2anc 673 . . . . . . . . . . . . . . . . . 18
183153simplrd 771 . . . . . . . . . . . . . . . . . . . 20
184183zred 11063 . . . . . . . . . . . . . . . . . . 19
185155, 15syl 17 . . . . . . . . . . . . . . . . . . 19
186184, 185remulcld 9689 . . . . . . . . . . . . . . . . . 18
187182, 186resubcld 10068 . . . . . . . . . . . . . . . . 17
188187rexrd 9708 . . . . . . . . . . . . . . . 16
189187ltpnfd 11446 . . . . . . . . . . . . . . . 16
190188, 176, 189xrltled 37574 . . . . . . . . . . . . . . 15
191 iooss2 11697 . . . . . . . . . . . . . . 15
192176, 190, 191syl2anc 673 . . . . . . . . . . . . . 14
193183adantr 472 . . . . . . . . . . . . . . . . . . . . 21
194193zcnd 11064 . . . . . . . . . . . . . . . . . . . 20
195185recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
196195adantr 472 . . . . . . . . . . . . . . . . . . . 20
197194, 196mulneg1d 10092 . . . . . . . . . . . . . . . . . . 19
198197oveq2d 6324 . . . . . . . . . . . . . . . . . 18
199 elioore 11691 . . . . . . . . . . . . . . . . . . . . . 22
200199recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
201200adantl 473 . . . . . . . . . . . . . . . . . . . 20
202194, 196mulcld 9681 . . . . . . . . . . . . . . . . . . . 20
203201, 202addcld 9680 . . . . . . . . . . . . . . . . . . 19
204203, 202negsubd 10011 . . . . . . . . . . . . . . . . . 18
205201, 202pncand 10006 . . . . . . . . . . . . . . . . . 18
206198, 204, 2053eqtrrd 2510 . . . . . . . . . . . . . . . . 17
207155adantr 472 . . . . . . . . . . . . . . . . . 18
208154simpld 466 . . . . . . . . . . . . . . . . . . . . 21 ..^
209 fourierdlem48.cn . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
210 cncff 22003 . . . . . . . . . . . . . . . . . . . . . . . 24
211 fdm 5745 . . . . . . . . . . . . . . . . . . . . . . . 24
212209, 210, 2113syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
213 ssdmres 5132 . . . . . . . . . . . . . . . . . . . . . . 23
214212, 213sylibr 217 . . . . . . . . . . . . . . . . . . . . . 22 ..^
215156, 162syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
216215adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ..^
217214, 216sseqtrd 3454 . . . . . . . . . . . . . . . . . . . . 21 ..^
218208, 217syl 17 . . . . . . . . . . . . . . . . . . . 20
219218adantr 472 . . . . . . . . . . . . . . . . . . 19
220 elfzofz 11962 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
221220adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
222178, 221ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
223155, 177, 222syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
224223rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21
225224adantr 472 . . . . . . . . . . . . . . . . . . . 20
226182rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21
227226adantr 472 . . . . . . . . . . . . . . . . . . . 20
228199adantl 473 . . . . . . . . . . . . . . . . . . . . 21
229193zred 11063 . . . . . . . . . . . . . . . . . . . . . 22
230207, 15syl 17 . . . . . . . . . . . . . . . . . . . . . 22
231229, 230remulcld 9689 . . . . . . . . . . . . . . . . . . . . 21
232228, 231readdcld 9688 . . . . . . . . . . . . . . . . . . . 20
233223adantr 472 . . . . . . . . . . . . . . . . . . . . 21
234155, 10syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
235234, 186readdcld 9688 . . . . . . . . . . . . . . . . . . . . . 22
236235adantr 472 . . . . . . . . . . . . . . . . . . . . 21
237152simprbi 471 . . . . . . . . . . . . . . . . . . . . . . . . 25
238237eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . 24
239154simprd 470 . . . . . . . . . . . . . . . . . . . . . . . 24
240238, 239eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . 23
241 icogelb 11711 . . . . . . . . . . . . . . . . . . . . . . 23
242224, 226, 240, 241syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22
243242adantr 472 . . . . . . . . . . . . . . . . . . . . 21
244207, 10syl 17 . . . . . . . . . . . . . . . . . . . . . 22
245244rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23
246182adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
247246, 231resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . 24
248247rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23
249 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23
250 ioogtlb 37688 . . . . . . . . . . . . . . . . . . . . . . 23
251245, 248, 249, 250syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22
252244, 228, 231, 251ltadd1dd 10245 . . . . . . . . . . . . . . . . . . . . 21
253233, 236, 232, 243, 252lelttrd 9810 . . . . . . . . . . . . . . . . . . . 20
254 iooltub 37706 . . . . . . . . . . . . . . . . . . . . . . 23
255245, 248, 249, 254syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . 22
256228, 247, 231, 255ltadd1dd 10245 . . . . . . . . . . . . . . . . . . . . 21
257182recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
258186recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
259257, 258npcand 10009 . . . . . . . . . . . . . . . . . . . . . 22
260259adantr 472 . . . . . . . . . . . . . . . . . . . . 21
261256, 260breqtrd 4420 . . . . . . . . . . . . . . . . . . . 20
262225, 227, 232, 253, 261eliood 37691 . . . . . . . . . . . . . . . . . . 19
263219, 262sseldd 3419 . . . . . . . . . . . . . . . . . 18
264193znegcld 11065 . . . . . . . . . . . . . . . . . 18
265 ovex 6336 . . . . . . . . . . . . . . . . . . 19
266 eleq1 2537 . . . . . . . . . . . . . . . . . . . . 21
2672663anbi2d 1370 . . . . . . . . . . . . . . . . . . . 20
268 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
269268eleq1d 2533 . . . . . . . . . . . . . . . . . . . 20
270267, 269imbi12d 327 . . . . . . . . . . . . . . . . . . 19
271 negex 9893 . . . . . . . . . . . . . . . . . . . 20
272 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . 22
2732723anbi3d 1371 . . . . . . . . . . . . . . . . . . . . 21
274 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . 23
275274oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . 22
276275eleq1d 2533 . . . . . . . . . . . . . . . . . . . . 21
277273, 276imbi12d 327 . . . . . . . . . . . . . . . . . . . 20
278 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . 23
2792783anbi3d 1371 . . . . . . . . . . . . . . . . . . . . . 22
280 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . 24
281280oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . 23
282281eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . 22
283279, 282imbi12d 327 . . . . . . . . . . . . . . . . . . . . 21
284 fourierdlem48.dper . . . . . . . . . . . . . . . . . . . . 21
285283, 284chvarv 2120 . . . . . . . . . . . . . . . . . . . 20
286271, 277, 285vtocl 3086 . . . . . . . . . . . . . . . . . . 19
287265, 270, 286vtocl 3086 . . . . . . . . . . . . . . . . . 18
288207, 263, 264, 287syl3anc 1292 . . . . . . . . . . . . . . . . 17
289206, 288eqeltrd 2549 . . . . . . . . . . . . . . . 16
290289ralrimiva 2809 . . . . . . . . . . . . . . 15
291 dfss3 3408 . . . . . . . . . . . . . . 15
292290, 291sylibr 217 . . . . . . . . . . . . . 14
293192, 292ssind 3647 . . . . . . . . . . . . 13
294 ioosscn 37687 . . . . . . . . . . . . . 14
295 ssinss1 3651 . . . . . . . . . . . . . 14
296294, 295mp1i 13 . . . . . . . . . . . . 13
297 eqid 2471 . . . . . . . . . . . . 13 fld fld
298 eqid 2471 . . . . . . . . . . . . 13 fldt fldt
299234rexrd 9708 . . . . . . . . . . . . . . 15
300234leidd 10201 . . . . . . . . . . . . . . 15
301237oveq1d 6323 . . . . . . . . . . . . . . . . 17
302234recnd 9687 . . . . . . . . . . . . . . . . . 18
303302, 258pncand 10006 . . . . . . . . . . . . . . . . 17
304301, 303eqtr2d 2506 . . . . . . . . . . . . . . . 16
305 icossre 11740 . . . . . . . . . . . . . . . . . . 19
306223, 226, 305syl2anc 673 . . . . . . . . . . . . . . . . . 18
307306, 239sseldd 3419 . . . . . . . . . . . . . . . . 17
308 icoltub 37703 . . . . . . . . . . . . . . . . . 18
309224, 226, 239, 308syl3anc 1292 . . . . . . . . . . . . . . . . 17
310307, 182, 186, 309ltsub1dd 10246 . . . . . . . . . . . . . . . 16
311304, 310eqbrtrd 4416 . . . . . . . . . . . . . . 15
312299, 188, 299, 300, 311elicod 11710 . . . . . . . . . . . . . 14
313 snunioo1 37709 . . . . . . . . . . . . . . . . 17
314299, 188, 311, 313syl3anc 1292 . . . . . . . . . . . . . . . 16
315314fveq2d 5883 . . . . . . . . . . . . . . 15 fldt fldt
316297cnfldtop 21882 . . . . . . . . . . . . . . . . . 18 fld
317 ovex 6336 . . . . . . . . . . . . . . . . . . . 20
318317inex1 4537 . . . . . . . . . . . . . . . . . . 19
319 snex 4641 . . . . . . . . . . . . . . . . . . 19
320318, 319unex 6608 . . . . . . . . . . . . . . . . . 18
321 resttop 20253 . . . . . . . . . . . . . . . . . 18 fld fldt
322316, 320, 321mp2an 686 . . . . . . . . . . . . . . . . 17 fldt
323322a1i 11 . . . . . . . . . . . . . . . 16 fldt
324 retop 21860 . . . . . . . . . . . . . . . . . . 19
325324a1i 11 . . . . . . . . . . . . . . . . . 18
326320a1i 11 . . . . . . . . . . . . . . . . . 18
327 iooretop 21864 . . . . . . . . . . . . . . . . . . 19
328327a1i 11 . . . . . . . . . . . . . . . . . 18
329 elrestr 15405 . . . . . . . . . . . . . . . . . 18 t
330325, 326, 328, 329syl3anc 1292 . . . . . . . . . . . . . . . . 17 t
331 mnfxr 11437 . . . . . . . . . . . . . . . . . . . . . 22
332331a1i 11 . . . . . . . . . . . . . . . . . . . . 21
333188adantr 472 . . . . . . . . . . . . . . . . . . . . 21
334 icossre 11740 . . . . . . . . . . . . . . . . . . . . . . 23
335234, 188, 334syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
336335sselda 3418 . . . . . . . . . . . . . . . . . . . . 21
337336mnfltd 11449 . . . . . . . . . . . . . . . . . . . . 21
338299adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
339 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22
340 icoltub 37703 . . . . . . . . . . . . . . . . . . . . . 22
341338, 333, 339, 340syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21
342332, 333, 336, 337, 341eliood 37691 . . . . . . . . . . . . . . . . . . . 20
343 ssnid 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25
344343a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
345 sneq 3969 . . . . . . . . . . . . . . . . . . . . . . . 24
346344, 345eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . 23
347 elun2 3593 . . . . . . . . . . . . . . . . . . . . . . 23
348346, 347syl 17 . . . . . . . . . . . . . . . . . . . . . 22
349348adantl 473 . . . . . . . . . . . . . . . . . . . . 21
350299ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
351175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
352336adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
353234ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
354 icogelb 11711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
355338, 333, 339, 354syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . 26
356355adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
357 neqne 2651 . . . . . . . . . . . . . . . . . . . . . . . . . 26
358357adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25
359353, 352, 356, 358leneltd 9806 . . . . . . . . . . . . . . . . . . . . . . . 24
360352ltpnfd 11446 . . . . . . . . . . . . . . . . . . . . . . . 24
361350, 351, 352, 359, 360eliood 37691 . . . . . . . . . . . . . . . . . . . . . . 23
362183zcnd 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363362, 195mulneg1d 10092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
364363oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
365364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
366 ioosscn 37687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367366sseli 3414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
368367adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
369258adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
370368, 369addcld 9680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
371370, 369negsubd 10011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
372368, 369pncand 10006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
373365, 371, 3723eqtrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
374186adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
375228, 374readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
376225, 227, 375, 253, 261eliood 37691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
377219, 376sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3782723anbi3d 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
379274oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
380379eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
381378, 380imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3822663anbi2d 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
383 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384383eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385382, 384imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
386265, 385, 285vtocl 3086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
387271, 381, 386vtocl 3086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
388207, 377, 264, 387syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
389373, 388eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
390389ralrimiva 2809 . . . . . . . . . . . . . . . . . . . . . . . . . 26
391390, 291sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . 25
392391ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
393188ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
394341adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
395350, 393, 352, 359, 394eliood 37691 . . . . . . . . . . . . . . . . . . . . . . . 24
396392, 395sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . 23
397361, 396elind 3609 . . . . . . . . . . . . . . . . . . . . . 22
398 elun1 3592 . . . . . . . . . . . . . . . . . . . . . 22
399397, 398syl 17 . . . . . . . . . . . . . . . . . . . . 21
400349, 399pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20
401342, 400elind 3609 . . . . . . . . . . . . . . . . . . 19
402299adantr 472 . . . . . . . . . . . . . . . . . . . 20
403188adantr 472 . . . . . . . . . . . . . . . . . . . 20
404 elinel1 3610 . . . . . . . . . . . . . . . . . . . . . . 23
405 elioore 11691 . . . . . . . . . . . . . . . . . . . . . . 23
406404, 405syl 17 . . . . . . . . . . . . . . . . . . . . . 22
407406rexrd 9708 . . . . . . . . . . . . . . . . . . . . 21
408407adantl 473 . . . . . . . . . . . . . . . . . . . 20
409 elinel2 3611 . . . . . . . . . . . . . . . . . . . . 21
410234adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
41188eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . 25
412411adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24
413410, 412eqled 9755 . . . . . . . . . . . . . . . . . . . . . . 23
414413adantlr 729 . . . . . . . . . . . . . . . . . . . . . 22
415 simpll 768 . . . . . . . . . . . . . . . . . . . . . . 23
416 simplr 770 . . . . . . . . . . . . . . . . . . . . . . . . 25
417 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
418 elsn 3973 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
419417, 418sylnibr 312 . . . . . . . . . . . . . . . . . . . . . . . . . 26
420419adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25
421 elunnel2 37423 . . . . . . . . . . . . . . . . . . . . . . . . 25
422416, 420, 421syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . 24
423 elinel1 3610 . . . . . . . . . . . . . . . . . . . . . . . 24
424422, 423syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
425234adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
426 elioore 11691 . . . . . . . . . . . . . . . . . . . . . . . . 25
427426adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24
428299adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
429175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
430 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25
431 ioogtlb 37688 . . . . . . . . . . . . . . . . . . . . . . . . 25
432428, 429, 430, 431syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . 24
433425, 427, 432ltled 9800 . . . . . . . . . . . . . . . . . . . . . . 23
434415, 424, 433syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
435414, 434pm2.61dan 808 . . . . . . . . . . . . . . . . . . . . 21
436409, 435sylan2 482 . . . . . . . . . . . . . . . . . . . 20
437331a1i 11 . . . . . . . . . . . . . . . . . . . . . 22