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

Theorem fourierdlem76 38158
 Description: Continuity of and its limits with respect to the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem76.f
fourierdlem76.xre
fourierdlem76.p ..^
fourierdlem76.m
fourierdlem76.v
fourierdlem76.fcn ..^
fourierdlem76.r ..^ lim
fourierdlem76.l ..^ lim
fourierdlem76.a
fourierdlem76.b
fourierdlem76.altb
fourierdlem76.ab
fourierdlem76.n0
fourierdlem76.c
fourierdlem76.o
fourierdlem76.q
fourierdlem76.t
fourierdlem76.n
fourierdlem76.s
fourierdlem76.d
fourierdlem76.e
fourierdlem76.ch ..^ ..^
Assertion
Ref Expression
fourierdlem76 ..^ ..^ lim lim
Distinct variable groups:   ,   ,   ,   ,   ,   ,,   ,,,   ,   ,   ,   ,   ,   ,   ,,,   ,   ,,,   ,,   ,   ,   ,,,
Allowed substitution hints:   (,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,,)   (,,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   (,,,,,)   (,,,,)   (,,,,)   (,)   (,,,,)   (,,,,,)   (,)   ()

Proof of Theorem fourierdlem76
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fourierdlem76.ch . . 3 ..^ ..^
2 eqid 2471 . . . . 5
3 eqid 2471 . . . . 5
4 eqid 2471 . . . . 5
5 simplll 776 . . . . . . . . . . 11 ..^ ..^
61, 5sylbi 200 . . . . . . . . . 10
76adantr 472 . . . . . . . . 9
8 ioossicc 11745 . . . . . . . . . 10
9 fourierdlem76.a . . . . . . . . . . . . . 14
109rexrd 9708 . . . . . . . . . . . . 13
116, 10syl 17 . . . . . . . . . . . 12
1211adantr 472 . . . . . . . . . . 11
13 fourierdlem76.b . . . . . . . . . . . . . 14
1413rexrd 9708 . . . . . . . . . . . . 13
156, 14syl 17 . . . . . . . . . . . 12
1615adantr 472 . . . . . . . . . . 11
17 elioore 11691 . . . . . . . . . . . 12
1817adantl 473 . . . . . . . . . . 11
196, 9syl 17 . . . . . . . . . . . . 13
2019adantr 472 . . . . . . . . . . . 12
21 fourierdlem76.t . . . . . . . . . . . . . . . . . . 19
22 prfi 7864 . . . . . . . . . . . . . . . . . . . . 21
2322a1i 11 . . . . . . . . . . . . . . . . . . . 20
24 fzfid 12224 . . . . . . . . . . . . . . . . . . . . 21
25 fourierdlem76.q . . . . . . . . . . . . . . . . . . . . . 22
2625rnmptfi 37508 . . . . . . . . . . . . . . . . . . . . 21
27 infi 7813 . . . . . . . . . . . . . . . . . . . . 21
2824, 26, 273syl 18 . . . . . . . . . . . . . . . . . . . 20
29 unfi 7856 . . . . . . . . . . . . . . . . . . . 20
3023, 28, 29syl2anc 673 . . . . . . . . . . . . . . . . . . 19
3121, 30syl5eqel 2553 . . . . . . . . . . . . . . . . . 18
32 prssg 4118 . . . . . . . . . . . . . . . . . . . . . 22
339, 13, 32syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
349, 13, 33mpbi2and 935 . . . . . . . . . . . . . . . . . . . 20
35 inss2 3644 . . . . . . . . . . . . . . . . . . . . . 22
36 ioossre 11721 . . . . . . . . . . . . . . . . . . . . . 22
3735, 36sstri 3427 . . . . . . . . . . . . . . . . . . . . 21
3837a1i 11 . . . . . . . . . . . . . . . . . . . 20
3934, 38unssd 3601 . . . . . . . . . . . . . . . . . . 19
4021, 39syl5eqss 3462 . . . . . . . . . . . . . . . . . 18
41 fourierdlem76.s . . . . . . . . . . . . . . . . . 18
42 fourierdlem76.n . . . . . . . . . . . . . . . . . 18
4331, 40, 41, 42fourierdlem36 38118 . . . . . . . . . . . . . . . . 17
446, 43syl 17 . . . . . . . . . . . . . . . 16
45 isof1o 6234 . . . . . . . . . . . . . . . 16
46 f1of 5828 . . . . . . . . . . . . . . . 16
4744, 45, 463syl 18 . . . . . . . . . . . . . . 15
486, 40syl 17 . . . . . . . . . . . . . . 15
4947, 48fssd 5750 . . . . . . . . . . . . . 14
5049adantr 472 . . . . . . . . . . . . 13
51 simpllr 777 . . . . . . . . . . . . . . . 16 ..^ ..^ ..^
521, 51sylbi 200 . . . . . . . . . . . . . . 15 ..^
53 elfzofz 11962 . . . . . . . . . . . . . . 15 ..^
5452, 53syl 17 . . . . . . . . . . . . . 14
5554adantr 472 . . . . . . . . . . . . 13
5650, 55ffvelrnd 6038 . . . . . . . . . . . 12
5743, 45, 463syl 18 . . . . . . . . . . . . . . . . . 18
58 frn 5747 . . . . . . . . . . . . . . . . . 18
5957, 58syl 17 . . . . . . . . . . . . . . . . 17
609leidd 10201 . . . . . . . . . . . . . . . . . . . . 21
61 fourierdlem76.altb . . . . . . . . . . . . . . . . . . . . . 22
629, 13, 61ltled 9800 . . . . . . . . . . . . . . . . . . . . 21
639, 13, 9, 60, 62eliccd 37697 . . . . . . . . . . . . . . . . . . . 20
6413leidd 10201 . . . . . . . . . . . . . . . . . . . . 21
659, 13, 13, 62, 64eliccd 37697 . . . . . . . . . . . . . . . . . . . 20
66 prssg 4118 . . . . . . . . . . . . . . . . . . . . 21
679, 13, 66syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
6863, 65, 67mpbi2and 935 . . . . . . . . . . . . . . . . . . 19
6935, 8sstri 3427 . . . . . . . . . . . . . . . . . . . 20
7069a1i 11 . . . . . . . . . . . . . . . . . . 19
7168, 70unssd 3601 . . . . . . . . . . . . . . . . . 18
7221, 71syl5eqss 3462 . . . . . . . . . . . . . . . . 17
7359, 72sstrd 3428 . . . . . . . . . . . . . . . 16
746, 73syl 17 . . . . . . . . . . . . . . 15
75 ffun 5742 . . . . . . . . . . . . . . . . 17
7649, 75syl 17 . . . . . . . . . . . . . . . 16
77 fdm 5745 . . . . . . . . . . . . . . . . . . 19
7849, 77syl 17 . . . . . . . . . . . . . . . . . 18
7978eqcomd 2477 . . . . . . . . . . . . . . . . 17
8054, 79eleqtrd 2551 . . . . . . . . . . . . . . . 16
81 fvelrn 6030 . . . . . . . . . . . . . . . 16
8276, 80, 81syl2anc 673 . . . . . . . . . . . . . . 15
8374, 82sseldd 3419 . . . . . . . . . . . . . 14
84 iccgelb 11716 . . . . . . . . . . . . . 14
8511, 15, 83, 84syl3anc 1292 . . . . . . . . . . . . 13
8685adantr 472 . . . . . . . . . . . 12
8756rexrd 9708 . . . . . . . . . . . . 13
88 fzofzp1 12037 . . . . . . . . . . . . . . . . 17 ..^
8952, 88syl 17 . . . . . . . . . . . . . . . 16
9049, 89ffvelrnd 6038 . . . . . . . . . . . . . . 15
9190rexrd 9708 . . . . . . . . . . . . . 14
9291adantr 472 . . . . . . . . . . . . 13
93 simpr 468 . . . . . . . . . . . . 13
94 ioogtlb 37688 . . . . . . . . . . . . 13
9587, 92, 93, 94syl3anc 1292 . . . . . . . . . . . 12
9620, 56, 18, 86, 95lelttrd 9810 . . . . . . . . . . 11
9790adantr 472 . . . . . . . . . . . 12
986, 13syl 17 . . . . . . . . . . . . 13
9998adantr 472 . . . . . . . . . . . 12
100 iooltub 37706 . . . . . . . . . . . . 13
10187, 92, 93, 100syl3anc 1292 . . . . . . . . . . . 12
10289, 79eleqtrd 2551 . . . . . . . . . . . . . . . 16
103 fvelrn 6030 . . . . . . . . . . . . . . . 16
10476, 102, 103syl2anc 673 . . . . . . . . . . . . . . 15
10574, 104sseldd 3419 . . . . . . . . . . . . . 14
106 iccleub 11715 . . . . . . . . . . . . . 14
10711, 15, 105, 106syl3anc 1292 . . . . . . . . . . . . 13
108107adantr 472 . . . . . . . . . . . 12
10918, 97, 99, 101, 108ltletrd 9812 . . . . . . . . . . 11
11012, 16, 18, 96, 109eliood 37691 . . . . . . . . . 10
1118, 110sseldi 3416 . . . . . . . . 9
112 fourierdlem76.f . . . . . . . . . . 11
113112adantr 472 . . . . . . . . . 10
114 fourierdlem76.xre . . . . . . . . . . . 12
115114adantr 472 . . . . . . . . . . 11
1169, 13iccssred 37698 . . . . . . . . . . . 12
117116sselda 3418 . . . . . . . . . . 11
118115, 117readdcld 9688 . . . . . . . . . 10
119113, 118ffvelrnd 6038 . . . . . . . . 9
1207, 111, 119syl2anc 673 . . . . . . . 8
121120recnd 9687 . . . . . . 7
122 fourierdlem76.c . . . . . . . . . 10
123122recnd 9687 . . . . . . . . 9
1246, 123syl 17 . . . . . . . 8
125124adantr 472 . . . . . . 7
126121, 125subcld 10005 . . . . . 6
127 ioossre 11721 . . . . . . . . 9
128127a1i 11 . . . . . . . 8
129128sselda 3418 . . . . . . 7
130129recnd 9687 . . . . . 6
131 nne 2647 . . . . . . . . . . . 12
132131biimpi 199 . . . . . . . . . . 11
133132eqcomd 2477 . . . . . . . . . 10
134133adantl 473 . . . . . . . . 9
135 simpr 468 . . . . . . . . . 10
136135adantr 472 . . . . . . . . 9
137134, 136eqeltrd 2549 . . . . . . . 8
138 fourierdlem76.n0 . . . . . . . . 9
139138ad2antrr 740 . . . . . . . 8
140137, 139condan 811 . . . . . . 7
1417, 111, 140syl2anc 673 . . . . . 6
142126, 130, 141divcld 10405 . . . . 5
143 2cnd 10704 . . . . . . 7
144130halfcld 10880 . . . . . . . 8
145144sincld 14261 . . . . . . 7
146143, 145mulcld 9681 . . . . . 6
14717recnd 9687 . . . . . . . . . 10
148147adantl 473 . . . . . . . . 9
149148halfcld 10880 . . . . . . . 8
150149sincld 14261 . . . . . . 7
151 2ne0 10724 . . . . . . . 8
152151a1i 11 . . . . . . 7
153 fourierdlem76.ab . . . . . . . . . . 11
1546, 153syl 17 . . . . . . . . . 10
155154adantr 472 . . . . . . . . 9
156155, 111sseldd 3419 . . . . . . . 8
157 fourierdlem44 38127 . . . . . . . 8
158156, 141, 157syl2anc 673 . . . . . . 7
159143, 150, 152, 158mulne0d 10286 . . . . . 6
160130, 146, 159divcld 10405 . . . . 5
161 eqid 2471 . . . . . 6
162 eqid 2471 . . . . . 6
163141neneqd 2648 . . . . . . . 8
164 elsn 3973 . . . . . . . 8
165163, 164sylnibr 312 . . . . . . 7
166130, 165eldifd 3401 . . . . . 6
167 eqid 2471 . . . . . . 7
168 eqid 2471 . . . . . . 7
169 elfzofz 11962 . . . . . . . . . . . . . . 15 ..^
170169adantl 473 . . . . . . . . . . . . . 14 ..^
171 pire 23492 . . . . . . . . . . . . . . . . . . . . 21
172171renegcli 9955 . . . . . . . . . . . . . . . . . . . 20
173172a1i 11 . . . . . . . . . . . . . . . . . . 19
174173, 114readdcld 9688 . . . . . . . . . . . . . . . . . 18
175171a1i 11 . . . . . . . . . . . . . . . . . . 19
176175, 114readdcld 9688 . . . . . . . . . . . . . . . . . 18
177174, 176iccssred 37698 . . . . . . . . . . . . . . . . 17
178177adantr 472 . . . . . . . . . . . . . . . 16 ..^
179 fourierdlem76.p . . . . . . . . . . . . . . . . . . 19 ..^
180 fourierdlem76.m . . . . . . . . . . . . . . . . . . 19
181 fourierdlem76.v . . . . . . . . . . . . . . . . . . 19
182179, 180, 181fourierdlem15 38096 . . . . . . . . . . . . . . . . . 18
183182adantr 472 . . . . . . . . . . . . . . . . 17 ..^
184183, 170ffvelrnd 6038 . . . . . . . . . . . . . . . 16 ..^
185178, 184sseldd 3419 . . . . . . . . . . . . . . 15 ..^
186114adantr 472 . . . . . . . . . . . . . . 15 ..^
187185, 186resubcld 10068 . . . . . . . . . . . . . 14 ..^
18825fvmpt2 5972 . . . . . . . . . . . . . 14
189170, 187, 188syl2anc 673 . . . . . . . . . . . . 13 ..^
190189, 187eqeltrd 2549 . . . . . . . . . . . 12 ..^
191190adantlr 729 . . . . . . . . . . 11 ..^ ..^
192191adantr 472 . . . . . . . . . 10 ..^ ..^
1931, 192sylbi 200 . . . . . . . . 9
194 fveq2 5879 . . . . . . . . . . . . . . . . . 18
195194oveq1d 6323 . . . . . . . . . . . . . . . . 17
196195cbvmptv 4488 . . . . . . . . . . . . . . . 16
19725, 196eqtri 2493 . . . . . . . . . . . . . . 15
198197a1i 11 . . . . . . . . . . . . . 14 ..^
199 fveq2 5879 . . . . . . . . . . . . . . . 16
200199oveq1d 6323 . . . . . . . . . . . . . . 15
201200adantl 473 . . . . . . . . . . . . . 14 ..^
202 fzofzp1 12037 . . . . . . . . . . . . . . 15 ..^
203202adantl 473 . . . . . . . . . . . . . 14 ..^
204183, 203ffvelrnd 6038 . . . . . . . . . . . . . . . 16 ..^
205178, 204sseldd 3419 . . . . . . . . . . . . . . 15 ..^
206205, 186resubcld 10068 . . . . . . . . . . . . . 14 ..^
207198, 201, 203, 206fvmptd 5969 . . . . . . . . . . . . 13 ..^
208207, 206eqeltrd 2549 . . . . . . . . . . . 12 ..^
209208adantlr 729 . . . . . . . . . . 11 ..^ ..^
210209adantr 472 . . . . . . . . . 10 ..^ ..^
2111, 210sylbi 200 . . . . . . . . 9
212179fourierdlem2 38083 . . . . . . . . . . . . . . . . . 18 ..^
213180, 212syl 17 . . . . . . . . . . . . . . . . 17 ..^
214181, 213mpbid 215 . . . . . . . . . . . . . . . 16 ..^
215214simprrd 775 . . . . . . . . . . . . . . 15 ..^
216215r19.21bi 2776 . . . . . . . . . . . . . 14 ..^
217185, 205, 186, 216ltsub1dd 10246 . . . . . . . . . . . . 13 ..^
218217, 189, 2073brtr4d 4426 . . . . . . . . . . . 12 ..^
219218adantlr 729 . . . . . . . . . . 11 ..^ ..^
220219adantr 472 . . . . . . . . . 10 ..^ ..^
2211, 220sylbi 200 . . . . . . . . 9
2221biimpi 199 . . . . . . . . . . . . . . . . . 18 ..^ ..^
223222simplrd 771 . . . . . . . . . . . . . . . . 17 ..^
2246, 223, 185syl2anc 673 . . . . . . . . . . . . . . . 16
225224rexrd 9708 . . . . . . . . . . . . . . 15
226225adantr 472 . . . . . . . . . . . . . 14
2276, 223, 205syl2anc 673 . . . . . . . . . . . . . . . 16
228227rexrd 9708 . . . . . . . . . . . . . . 15
229228adantr 472 . . . . . . . . . . . . . 14
2306, 114syl 17 . . . . . . . . . . . . . . . 16
231230adantr 472 . . . . . . . . . . . . . . 15
232 elioore 11691 . . . . . . . . . . . . . . . 16
233232adantl 473 . . . . . . . . . . . . . . 15
234231, 233readdcld 9688 . . . . . . . . . . . . . 14
2356, 223, 189syl2anc 673 . . . . . . . . . . . . . . . . . 18
236235oveq2d 6324 . . . . . . . . . . . . . . . . 17
237230recnd 9687 . . . . . . . . . . . . . . . . . 18
238224recnd 9687 . . . . . . . . . . . . . . . . . 18
239237, 238pncan3d 10008 . . . . . . . . . . . . . . . . 17
240236, 239eqtr2d 2506 . . . . . . . . . . . . . . . 16
241240adantr 472 . . . . . . . . . . . . . . 15
242193adantr 472 . . . . . . . . . . . . . . . 16
243193rexrd 9708 . . . . . . . . . . . . . . . . . 18
244243adantr 472 . . . . . . . . . . . . . . . . 17
245211rexrd 9708 . . . . . . . . . . . . . . . . . 18
246245adantr 472 . . . . . . . . . . . . . . . . 17
247 simpr 468 . . . . . . . . . . . . . . . . 17
248 ioogtlb 37688 . . . . . . . . . . . . . . . . 17
249244, 246, 247, 248syl3anc 1292 . . . . . . . . . . . . . . . 16
250242, 233, 231, 249ltadd2dd 9811 . . . . . . . . . . . . . . 15
251241, 250eqbrtrd 4416 . . . . . . . . . . . . . 14
252211adantr 472 . . . . . . . . . . . . . . . 16
253 iooltub 37706 . . . . . . . . . . . . . . . . 17
254244, 246, 247, 253syl3anc 1292 . . . . . . . . . . . . . . . 16
255233, 252, 231, 254ltadd2dd 9811 . . . . . . . . . . . . . . 15
2566, 223, 207syl2anc 673 . . . . . . . . . . . . . . . . . 18
257256oveq2d 6324 . . . . . . . . . . . . . . . . 17
258227recnd 9687 . . . . . . . . . . . . . . . . . 18
259237, 258pncan3d 10008 . . . . . . . . . . . . . . . . 17
260257, 259eqtrd 2505 . . . . . . . . . . . . . . . 16
261260adantr 472 . . . . . . . . . . . . . . 15
262255, 261breqtrd 4420 . . . . . . . . . . . . . 14
263226, 229, 234, 251, 262eliood 37691 . . . . . . . . . . . . 13
264 fvres 5893 . . . . . . . . . . . . 13
265263, 264syl 17 . . . . . . . . . . . 12
266265eqcomd 2477 . . . . . . . . . . 11
267266mpteq2dva 4482 . . . . . . . . . 10
268 ioosscn 37687 . . . . . . . . . . . 12
269268a1i 11 . . . . . . . . . . 11
270 fourierdlem76.fcn . . . . . . . . . . . 12 ..^
2716, 223, 270syl2anc 673 . . . . . . . . . . 11
272 ioosscn 37687 . . . . . . . . . . . 12
273272a1i 11 . . . . . . . . . . 11
274269, 271, 273, 237, 263fourierdlem23 38104 . . . . . . . . . 10
275267, 274eqeltrd 2549 . . . . . . . . 9
2766, 112syl 17 . . . . . . . . . 10
277 ioossre 11721 . . . . . . . . . . 11
278277a1i 11 . . . . . . . . . 10
279 eqid 2471 . . . . . . . . . 10
280 ioossre 11721 . . . . . . . . . . 11
281280a1i 11 . . . . . . . . . 10
282233, 254ltned 9788 . . . . . . . . . 10
283 fourierdlem76.l . . . . . . . . . . . 12 ..^ lim
2846, 223, 283syl2anc 673 . . . . . . . . . . 11 lim
285260eqcomd 2477 . . . . . . . . . . . 12
286285oveq2d 6324 . . . . . . . . . . 11 lim lim
287284, 286eleqtrd 2551 . . . . . . . . . 10 lim
288211recnd 9687 . . . . . . . . . 10
289276, 230, 278, 279, 263, 281, 282, 287, 288fourierdlem53 38135 . . . . . . . . 9 lim
29049, 54ffvelrnd 6038 . . . . . . . . 9
291 elfzoelz 11947 . . . . . . . . . . . 12 ..^
292 zre 10965 . . . . . . . . . . . 12
29352, 291, 2923syl 18 . . . . . . . . . . 11
294293ltp1d 10559 . . . . . . . . . 10
295 isorel 6235 . . . . . . . . . . 11
29644, 54, 89, 295syl12anc 1290 . . . . . . . . . 10
297294, 296mpbid 215 . . . . . . . . 9
2981simprbi 471 . . . . . . . . 9
299 eqid 2471 . . . . . . . . 9
300 eqid 2471 . . . . . . . . 9 fldt fldt
301193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300fourierdlem33 38115 . . . . . . . 8 lim
302 eqidd 2472 . . . . . . . . . 10
303 simpr 468 . . . . . . . . . . . 12
304303oveq2d 6324 . . . . . . . . . . 11
305304fveq2d 5883 . . . . . . . . . 10
306243adantr 472 . . . . . . . . . . 11
307245adantr 472 . . . . . . . . . . 11
30890adantr 472 . . . . . . . . . . 11
309193, 211, 290, 90, 297, 298fourierdlem10 38091 . . . . . . . . . . . . . 14
310309simpld 466 . . . . . . . . . . . . 13
311193, 290, 90, 310, 297lelttrd 9810 . . . . . . . . . . . 12
312311adantr 472 . . . . . . . . . . 11
313211adantr 472 . . . . . . . . . . . 12
314309simprd 470 . . . . . . . . . . . . 13
315314adantr 472 . . . . . . . . . . . 12
316 neqne 2651 . . . . . . . . . . . . . 14
317316necomd 2698 . . . . . . . . . . . . 13
318317adantl 473 . . . . . . . . . . . 12
319308, 313, 315, 318leneltd 9806 . . . . . . . . . . 11
320306, 307, 308, 312, 319eliood 37691 . . . . . . . . . 10
321230, 90readdcld 9688 . . . . . . . . . . . 12
322276, 321ffvelrnd 6038 . . . . . . . . . . 11
323322adantr 472 . . . . . . . . . 10
324302, 305, 320, 323fvmptd 5969 . . . . . . . . 9
325324ifeq2da 3903 . . . . . . . 8
326298resmptd 5162 . . . . . . . . 9
327326oveq1d 6323 . . . . . . . 8 lim lim
328301, 325, 3273eltr3d 2563 . . . . . . 7 lim
329 ax-resscn 9614 . . . . . . . . 9
330128, 329syl6ss 3430 . . . . . . . 8
33190recnd 9687 . . . . . . . 8
332168, 330, 124, 331constlimc 37801 . . . . . . 7 lim
333167, 168, 161, 121, 125, 328, 332sublimc 37830 . . . . . 6 lim
334330, 162, 331idlimc 37803 . . . . . 6 lim
3356, 105jca 541 . . . . . . 7
336 eleq1 2537 . . . . . . . . . 10
337336anbi2d 718 . . . . . . . . 9
338 neeq1 2705 . . . . . . . . 9
339337, 338imbi12d 327 . . . . . . . 8
340339, 140vtoclg 3093 . . . . . . 7
34190, 335, 340sylc 61 . . . . . 6
342161, 162, 2, 126, 166, 333, 334, 341, 141divlimc 37834 . . . . 5 lim
343 eqid 2471 . . . . . 6
344143, 150mulcld 9681 . . . . . . 7
345159neneqd 2648 . . . . . . . 8
346 2re 10701 . . . . . . . . . . 11
347346a1i 11 . . . . . . . . . 10
34817rehalfcld 10882 . . . . . . . . . . . 12
349348resincld 14274 . . . . . . . . . . 11
350349adantl 473 . . . . . . . . . 10
351347, 350remulcld 9689 . . . . . . . . 9
352 elsncg 3983 . . . . . . . . 9
353351, 352syl 17 . . . . . . . 8
354345, 353mtbird 308 . . . . . . 7
355344, 354eldifd 3401 . . . . . 6
356 eqid 2471 . . . . . . 7
357 eqid 2471 . . . . . . 7
358 2cnd 10704 . . . . . . . 8
359356, 330, 358, 331constlimc 37801 . . . . . . 7 lim
360348ad2antrl 742 . . . . . . . 8
361 recn 9647 . . . . . . . . . 10
362361sincld 14261 . . . . . . . . 9
363362adantl 473 . . . . . . . 8
364 eqid 2471 . . . . . . . . 9
365 2cn 10702 . . . . . . . . . . 11
366 eldifsn 4088 . . . . . . . . . . 11
367365, 151, 366mpbir2an 934 . . . . . . . . . 10
368367a1i 11 . . . . . . . . 9
369151a1i 11 . . . . . . . . 9
370162, 356, 364, 148, 368, 334, 359, 369, 152divlimc 37834 . . . . . . . 8 lim
371 sinf 14255 . . . . . . . . . . . . . 14
372371a1i 11 . . . . . . . . . . . . 13
373329a1i 11 . . . . . . . . . . . . 13
374372, 373feqresmpt 5933 . . . . . . . . . . . 12
375374trud 1461 . . . . . . . . . . 11
376 resincncf 37849 . . . . . . . . . . 11
377375, 376eqeltrri 2546 . . . . . . . . . 10
378377a1i 11 . . . . . . . . 9
37990rehalfcld 10882 . . . . . . . . 9
380 fveq2 5879 . . . . . . . . 9
381378, 379, 380cnmptlimc 22924 . . . . . . . 8 lim
382 fveq2 5879 . . . . . . . 8
383 fveq2 5879 . . . . . . . . 9
384383ad2antll 743 . . . . . . . 8
385360, 363, 370, 381, 382, 384limcco 22927 . . . . . . 7 lim
386356, 357, 343, 143, 150, 359, 385mullimc 37793 . . . . . 6 lim
387331halfcld 10880 . . . . . . . 8
388387sincld 14261 . . . . . . 7
389154, 105sseldd 3419 . . . . . . . 8
390 fourierdlem44 38127 . . . . . . . 8
391389, 341, 390syl2anc 673 . . . . . . 7
392358, 388, 369, 391mulne0d 10286 . . . . . 6
393162, 343, 3, 148, 355, 334, 386, 392, 159divlimc 37834 . . . . 5 lim
3942, 3, 4, 142, 160, 342, 393mullimc 37793 . . . 4 lim
395 fourierdlem76.d . . . . 5
396395a1i 11 . . . 4
397 fourierdlem76.o . . . . . . 7
398397reseq1i 5107 . . . . . 6
399 ioossicc 11745 . . . . . . . 8
400 iccss 11727 . . . . . . . . 9
40119, 98, 85, 107, 400syl22anc 1293 . . . . . . . 8
402399, 401syl5ss 3429 . . . . . . 7
403402resmptd 5162 . . . . . 6
404398, 403syl5eq 2517 . . . . 5
405404oveq1d 6323 . . . 4 lim lim
406394, 396, 4053eltr4d 2564 . . 3 lim
4071, 406sylbir 218 . 2 ..^ ..^ lim
408242, 249gtned 9787 . . . . . . . . . 10
409 fourierdlem76.r . . . . . . . . . . . 12 ..^ lim
4106, 223, 409syl2anc 673 . . . . . . . . . . 11 lim
411240oveq2d 6324 . . . . . . . . . . 11 lim lim
412410, 411eleqtrd 2551 . . . . . . . . . 10 lim
413193recnd 9687 . . . . . . . . . 10
414276, 230, 278, 279, 263, 281, 408, 412, 413fourierdlem53 38135 . . . . . . . . 9 lim
415 eqid 2471 . . . . . . . . 9
416 eqid 2471 . . . . . . . . 9 fldt fldt
417193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416fourierdlem32 38114 . . . . . . . 8 lim
418 eqidd 2472 . . . . . . . . . 10
419 oveq2 6316 . . . . . . . . . . . 12
420419fveq2d 5883 . . . . . . . . . . 11
421420adantl 473 . . . . . . . . . 10
422243adantr 472 . . . . . . . . . . 11
423245adantr 472 . . . . . . . . . . 11
424290adantr 472 . . . . . . . . . . 11
425193adantr 472 . . . . . . . . . . . 12