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

Theorem fourierdlem46 31776
 Description: The function has a limit at the bounds of every interval induced by the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem46.cn
fourierdlem46.rlim lim
fourierdlem46.llim lim
fourierdlem46.qiso
fourierdlem46.qf
fourierdlem46.i ..^
fourierdlem46.10
fourierdlem46.qiss
fourierdlem46.c
fourierdlem46.h
fourierdlem46.ranq
Assertion
Ref Expression
fourierdlem46 lim lim
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem fourierdlem46
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fourierdlem46.h . . . . . . . . 9
2 pire 22718 . . . . . . . . . . . . . 14
32a1i 11 . . . . . . . . . . . . 13
43renegcld 9998 . . . . . . . . . . . 12
5 fourierdlem46.c . . . . . . . . . . . 12
64, 3, 53jca 1176 . . . . . . . . . . 11
7 tpssi 4199 . . . . . . . . . . 11
86, 7syl 16 . . . . . . . . . 10
94, 3iccssred 31426 . . . . . . . . . . 11
109ssdifssd 3647 . . . . . . . . . 10
118, 10unssd 3685 . . . . . . . . 9
121, 11syl5eqss 3553 . . . . . . . 8
13 fourierdlem46.qf . . . . . . . . 9
14 fourierdlem46.i . . . . . . . . . 10 ..^
15 elfzofz 11823 . . . . . . . . . 10 ..^
1614, 15syl 16 . . . . . . . . 9
1713, 16ffvelrnd 6033 . . . . . . . 8
1812, 17sseldd 3510 . . . . . . 7
1918adantr 465 . . . . . 6
20 fzofzp1 11889 . . . . . . . . . . 11 ..^
2114, 20syl 16 . . . . . . . . . 10
2213, 21ffvelrnd 6033 . . . . . . . . 9
2312, 22sseldd 3510 . . . . . . . 8
2423rexrd 9655 . . . . . . 7
2524adantr 465 . . . . . 6
26 fourierdlem46.10 . . . . . . 7
2726adantr 465 . . . . . 6
28 simpr 461 . . . . . . . . . . . . 13
29 simpl 457 . . . . . . . . . . . . 13
3028, 29eqeltrd 2555 . . . . . . . . . . . 12
3130adantll 713 . . . . . . . . . . 11
3231adantlr 714 . . . . . . . . . 10
33 ssun2 3673 . . . . . . . . . . . . . . . . . . 19
3433, 1sseqtr4i 3542 . . . . . . . . . . . . . . . . . 18
35 fourierdlem46.qiss . . . . . . . . . . . . . . . . . . . . . . 23
36 ioossicc 11622 . . . . . . . . . . . . . . . . . . . . . . 23
3735, 36syl6ss 3521 . . . . . . . . . . . . . . . . . . . . . 22
3837adantr 465 . . . . . . . . . . . . . . . . . . . . 21
39 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
4038, 39sseldd 3510 . . . . . . . . . . . . . . . . . . . 20
4140adantr 465 . . . . . . . . . . . . . . . . . . 19
42 simpr 461 . . . . . . . . . . . . . . . . . . 19
4341, 42eldifd 3492 . . . . . . . . . . . . . . . . . 18
4434, 43sseldi 3507 . . . . . . . . . . . . . . . . 17
45 fourierdlem46.ranq . . . . . . . . . . . . . . . . . . 19
4645eqcomd 2475 . . . . . . . . . . . . . . . . . 18
4746ad2antrr 725 . . . . . . . . . . . . . . . . 17
4844, 47eleqtrd 2557 . . . . . . . . . . . . . . . 16
49 simpr 461 . . . . . . . . . . . . . . . . . . . 20
50 ffn 5737 . . . . . . . . . . . . . . . . . . . . . . 23
5113, 50syl 16 . . . . . . . . . . . . . . . . . . . . . 22
5251adantr 465 . . . . . . . . . . . . . . . . . . . . 21
53 fvelrnb 5921 . . . . . . . . . . . . . . . . . . . . 21
5452, 53syl 16 . . . . . . . . . . . . . . . . . . . 20
5549, 54mpbid 210 . . . . . . . . . . . . . . . . . . 19
5655adantlr 714 . . . . . . . . . . . . . . . . . 18
57 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . 22
5857ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21
59 simplll 757 . . . . . . . . . . . . . . . . . . . . . . 23
60 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23
61 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25
62 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . 25
6361, 62eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . 24
6463adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23
65 elfzoelz 11809 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
6614, 65syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
6766ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
6818rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6968ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7024ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
71 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
72 ioogtlb 31415 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7369, 70, 71, 72syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
74 fourierdlem46.qiso . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7574ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7616ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
77 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . 26
78 isorel 6221 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7975, 76, 77, 78syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . 25
8073, 79mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24
81 iooltub 31435 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8269, 70, 71, 81syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
8321ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
84 isorel 6221 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8575, 77, 83, 84syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . 25
8682, 85mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24
87 btwnnz 10949 . . . . . . . . . . . . . . . . . . . . . . . 24
8867, 80, 86, 87syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
8959, 60, 64, 88syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . 22
9089adantllr 718 . . . . . . . . . . . . . . . . . . . . 21
9158, 90pm2.65da 576 . . . . . . . . . . . . . . . . . . . 20
9291ralrimiva 2881 . . . . . . . . . . . . . . . . . . 19
93 ralnex 2913 . . . . . . . . . . . . . . . . . . 19
9492, 93sylib 196 . . . . . . . . . . . . . . . . . 18
9556, 94pm2.65da 576 . . . . . . . . . . . . . . . . 17
9695adantr 465 . . . . . . . . . . . . . . . 16
9748, 96condan 792 . . . . . . . . . . . . . . 15
9897ralrimiva 2881 . . . . . . . . . . . . . 14
99 dfss3 3499 . . . . . . . . . . . . . 14
10098, 99sylibr 212 . . . . . . . . . . . . 13
101100ad2antrr 725 . . . . . . . . . . . 12
10268ad2antrr 725 . . . . . . . . . . . . 13
10324ad2antrr 725 . . . . . . . . . . . . 13
104 icossre 11617 . . . . . . . . . . . . . . . . 17
10518, 24, 104syl2anc 661 . . . . . . . . . . . . . . . 16
106105adantr 465 . . . . . . . . . . . . . . 15
107 simpr 461 . . . . . . . . . . . . . . 15
108106, 107sseldd 3510 . . . . . . . . . . . . . 14
109108adantr 465 . . . . . . . . . . . . 13
11018ad2antrr 725 . . . . . . . . . . . . . 14
11168adantr 465 . . . . . . . . . . . . . . . 16
11224adantr 465 . . . . . . . . . . . . . . . 16
113 icogelb 31429 . . . . . . . . . . . . . . . 16
114111, 112, 107, 113syl3anc 1228 . . . . . . . . . . . . . . 15
115114adantr 465 . . . . . . . . . . . . . 14
116 neqne 31339 . . . . . . . . . . . . . . 15
117116adantl 466 . . . . . . . . . . . . . 14
118110, 109, 115, 117leneltd 31394 . . . . . . . . . . . . 13
119 icoltub 31432 . . . . . . . . . . . . . . 15
120111, 112, 107, 119syl3anc 1228 . . . . . . . . . . . . . 14
121120adantr 465 . . . . . . . . . . . . 13
122102, 103, 109, 118, 121eliood 31418 . . . . . . . . . . . 12
123101, 122sseldd 3510 . . . . . . . . . . 11
124123adantllr 718 . . . . . . . . . 10
12532, 124pm2.61dan 789 . . . . . . . . 9
126125ralrimiva 2881 . . . . . . . 8
127 dfss3 3499 . . . . . . . 8
128126, 127sylibr 212 . . . . . . 7
129 fourierdlem46.cn . . . . . . . 8
130129adantr 465 . . . . . . 7
131 rescncf 21269 . . . . . . 7
132128, 130, 131sylc 60 . . . . . 6
13319, 25, 27, 132icocncflimc 31551 . . . . 5 lim
13418leidd 10131 . . . . . . . . . 10
13568, 24, 68, 134, 26elicod 31438 . . . . . . . . 9
136 fvres 5886 . . . . . . . . 9
137135, 136syl 16 . . . . . . . 8
138137eqcomd 2475 . . . . . . 7
139138adantr 465 . . . . . 6
140 ioossico 11625 . . . . . . . . . 10
141140a1i 11 . . . . . . . . 9
142141resabs1d 5309 . . . . . . . 8
143142eqcomd 2475 . . . . . . 7
144143oveq1d 6310 . . . . . 6 lim lim
145139, 144eleq12d 2549 . . . . 5 lim lim
146133, 145mpbird 232 . . . 4 lim
147 ne0i 3796 . . . 4 lim lim
148146, 147syl 16 . . 3 lim
149 pnfxr 11333 . . . . . . . . . 10
150149a1i 11 . . . . . . . . 9
15123ltpnfd 31380 . . . . . . . . . 10
15224, 150, 151xrltled 31356 . . . . . . . . 9
153 iooss2 11577 . . . . . . . . 9
154150, 152, 153syl2anc 661 . . . . . . . 8
155 resabs1 5308 . . . . . . . 8
156154, 155syl 16 . . . . . . 7
157156oveq1d 6310 . . . . . 6 lim lim
158157eqcomd 2475 . . . . 5 lim lim
159158adantr 465 . . . 4 lim lim
160 limcresi 22157 . . . . . 6 lim lim
161160a1i 11 . . . . 5 lim lim
16218adantr 465 . . . . . 6
163 simpl 457 . . . . . . 7
1642renegcli 9892 . . . . . . . . . . . 12
165164rexri 9658 . . . . . . . . . . 11
166165a1i 11 . . . . . . . . . 10
1672rexri 9658 . . . . . . . . . . 11
168167a1i 11 . . . . . . . . . 10
169166, 168, 68, 24, 26ioossioobi 31444 . . . . . . . . . . . 12
17035, 169mpbid 210 . . . . . . . . . . 11
171170simpld 459 . . . . . . . . . 10
172170simprd 463 . . . . . . . . . . 11
17318, 23, 3, 26, 172ltletrd 9753 . . . . . . . . . 10
174166, 168, 68, 171, 173elicod 31438 . . . . . . . . 9
175163, 174syl 16 . . . . . . . 8
176 simpr 461 . . . . . . . 8
177175, 176eldifd 3492 . . . . . . 7
178163, 177jca 532 . . . . . 6
179 eleq1 2539 . . . . . . . . 9
180179anbi2d 703 . . . . . . . 8
181 oveq1 6302 . . . . . . . . . . 11
182181reseq2d 5279 . . . . . . . . . 10
183 id 22 . . . . . . . . . 10
184182, 183oveq12d 6313 . . . . . . . . 9 lim lim
185184neeq1d 2744 . . . . . . . 8 lim lim
186180, 185imbi12d 320 . . . . . . 7 lim lim
187 fourierdlem46.rlim . . . . . . 7 lim
188186, 187vtoclg 3176 . . . . . 6 lim
189162, 178, 188sylc 60 . . . . 5 lim
190 ssn0 3823 . . . . 5 lim lim lim lim
191161, 189, 190syl2anc 661 . . . 4 lim
192159, 191eqnetrd 2760 . . 3 lim
193148, 192pm2.61dan 789 . 2 lim
19468adantr 465 . . . . . 6
19523adantr 465 . . . . . 6
19626adantr 465 . . . . . 6
197 simpr 461 . . . . . . . . . . . . 13
198 simpl 457 . . . . . . . . . . . . 13
199197, 198eqeltrd 2555 . . . . . . . . . . . 12
200199adantll 713 . . . . . . . . . . 11
201200adantlr 714 . . . . . . . . . 10
202100ad2antrr 725 . . . . . . . . . . . 12
20368ad2antrr 725 . . . . . . . . . . . . 13
20424ad2antrr 725 . . . . . . . . . . . . 13
20568adantr 465 . . . . . . . . . . . . . . . 16
20623adantr 465 . . . . . . . . . . . . . . . 16
207 iocssre 11616 . . . . . . . . . . . . . . . 16
208205, 206, 207syl2anc 661 . . . . . . . . . . . . . . 15
209 simpr 461 . . . . . . . . . . . . . . 15
210208, 209sseldd 3510 . . . . . . . . . . . . . 14
211210adantr 465 . . . . . . . . . . . . 13
21224adantr 465 . . . . . . . . . . . . . . 15
213 iocgtlb 31422 . . . . . . . . . . . . . . 15
214205, 212, 209, 213syl3anc 1228 . . . . . . . . . . . . . 14
215214adantr 465 . . . . . . . . . . . . 13
216206adantr 465 . . . . . . . . . . . . . 14
217 iocleub 31423 . . . . . . . . . . . . . . . 16
218205, 212, 209, 217syl3anc 1228 . . . . . . . . . . . . . . 15
219218adantr 465 . . . . . . . . . . . . . 14
220 neqne 31339 . . . . . . . . . . . . . . . 16
221220necomd 2738 . . . . . . . . . . . . . . 15
222221adantl 466 . . . . . . . . . . . . . 14
223211, 216, 219, 222leneltd 31394 . . . . . . . . . . . . 13
224203, 204, 211, 215, 223eliood 31418 . . . . . . . . . . . 12
225202, 224sseldd 3510 . . . . . . . . . . 11
226225adantllr 718 . . . . . . . . . 10
227201, 226pm2.61dan 789 . . . . . . . . 9
228227ralrimiva 2881 . . . . . . . 8
229 dfss3 3499 . . . . . . . 8
230228, 229sylibr 212 . . . . . . 7
231129adantr 465 . . . . . . 7
232 rescncf 21269 . . . . . . 7
233230, 231, 232sylc 60 . . . . . 6
234194, 195, 196, 233ioccncflimc 31547 . . . . 5 lim
23523leidd 10131 . . . . . . . . . 10
23668, 24, 24, 26, 235eliocd 31430 . . . . . . . . 9
237 fvres 5886 . . . . . . . . 9
238236, 237syl 16 . . . . . . . 8
239238eqcomd 2475 . . . . . . 7
240 ioossioc 31411 . . . . . . . . . . 11
241 resabs1 5308 . . . . . . . . . . 11
242240, 241ax-mp 5 . . . . . . . . . 10
243242eqcomi 2480 . . . . . . . . 9
244243oveq1i 6305 . . . . . . . 8 lim lim
245244a1i 11 . . . . . . 7 lim lim
246239, 245eleq12d 2549 . . . . . 6 lim lim
247246adantr 465 . . . . 5 lim lim
248234, 247mpbird 232 . . . 4 lim
249 ne0i 3796 . . . 4 lim lim
250248, 249syl 16 . . 3 lim
251 mnfxr 11335 . . . . . . . . . 10
252251a1i 11 . . . . . . . . 9
25318mnfltd 31391 . . . . . . . . . 10
254252, 68, 253xrltled 31356 . . . . . . . . 9
255 iooss1 11576 . . . . . . . . 9
256252, 254, 255syl2anc 661 . . . . . . . 8
257256resabs1d 5309 . . . . . . 7
258257eqcomd 2475 . . . . . 6
259258adantr 465 . . . . 5
260259oveq1d 6310 . . . 4 lim lim
261 limcresi 22157 . . . . . . 7 lim lim
262261a1i 11 . . . . . 6 lim lim
26323adantr 465 . . . . . . 7
264 simpl 457 . . . . . . . 8
265165a1i 11 . . . . . . . . . 10
266167a1i 11 . . . . . . . . . 10
267264, 24syl 16 . . . . . . . . . 10
2684, 18, 23, 171, 26lelttrd 9751 . . . . . . . . . . 11
269268adantr 465 . . . . . . . . . 10
270264, 172syl 16 . . . . . . . . . 10
271265, 266, 267, 269, 270eliocd 31430 . . . . . . . . 9
272 simpr 461 . . . . . . . . 9
273271, 272eldifd 3492 . . . . . . . 8
274264, 273jca 532 . . . . . . 7
275 eleq1 2539 . . . . . . . . . 10
276275anbi2d 703 . . . . . . . . 9
277 oveq2 6303 . . . . . . . . . . . 12
278277reseq2d 5279 . . . . . . . . . . 11
279 id 22 . . . . . . . . . . 11
280278, 279oveq12d 6313 . . . . . . . . . 10 lim lim
281280neeq1d 2744 . . . . . . . . 9 lim lim
282276, 281imbi12d 320 . . . . . . . 8 lim lim
283 fourierdlem46.llim . . . . . . . 8 lim
284282, 283vtoclg 3176 . . . . . . 7 lim
285263, 274, 284sylc 60 . . . . . 6 lim
286262, 285jca 532 . . . . 5 lim lim lim
287 ssn0 3823 . . . . 5 lim lim lim lim
288286, 287syl 16 . . . 4 lim
289260, 288eqnetrd 2760 . . 3 lim
290250, 289pm2.61dan 789 . 2 lim
291193, 290jca 532 1 lim lim
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 973   wceq 1379   wcel 1767   wne 2662  wral 2817  wrex 2818   cdif 3478   cun 3479   wss 3481  c0 3790  ctp 4037   class class class wbr 4453   cdm 5005   crn 5006   cres 5007   wfn 5589  wf 5590  cfv 5594   wiso 5595  (class class class)co 6295  cc 9502  cr 9503  cc0 9504  c1 9505   caddc 9507   cpnf 9637   cmnf 9638  cxr 9639   clt 9640   cle 9641  cneg 9818  cz 10876  cioo 11541  cioc 11542  cico 11543  cicc 11544  cfz 11684  ..^cfzo 11804  cpi 13681  ccncf 21248   lim climc 22134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-er 7323  df-map 7434  df-pm 7435  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-seq 12088  df-exp 12147  df-fac 12334  df-bc 12361  df-hash 12386  df-shft 12880  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-limsup 13274  df-clim 13291  df-rlim 13292  df-sum 13489  df-ef 13682  df-sin 13684  df-cos 13685  df-pi 13687  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-fbas 18286  df-fg 18287  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-perf 19506  df-cn 19596  df-cnp 19597  df-haus 19684  df-tx 19931  df-hmeo 20124  df-fil 20215  df-fm 20307  df-flim 20308  df-flf 20309  df-xms 20691  df-ms 20692  df-tms 20693  df-cncf 21250  df-limc 22138  df-dv 22139 This theorem is referenced by:  fourierdlem102  31832  fourierdlem114  31844
 Copyright terms: Public domain W3C validator