fourierdlem62 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem62 40385

Description: The function

is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypothesis**
Ref	Expression
fourierdlem62.k

**Assertion**
Ref	Expression
fourierdlem62

Proof of Theorem fourierdlem62 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem62.k	. . . 4
2		eqeq1 2626	. . . . . 6
3		id 22	. . . . . . 7
4		oveq1 6657	. . . . . . . . 9
5	4	fveq2d 6195	. . . . . . . 8
6	5	oveq2d 6666	. . . . . . 7
7	3, 6	oveq12d 6668	. . . . . 6
8	2, 7	ifbieq2d 4111	. . . . 5
9	8	cbvmptv 4750	. . . 4
10	1, 9	eqtri 2644	. . 3
11	10	fourierdlem43 40367	. 2
12		ax-resscn 9993	. . 3
13		fss 6056	. . . . . 6 $/\$
14	11, 12, 13	mp2an 708	. . . . 5
15	14	a1i 11	. . . . . . . . 9
16		difss 3737	. . . . . . . . . . . . . . . . 17 $\$
17		elioore 12205	. . . . . . . . . . . . . . . . . 18
18	17	ssriv 3607	. . . . . . . . . . . . . . . . 17
19	16, 18	sstri 3612	. . . . . . . . . . . . . . . 16 $\$
20	19	a1i 11	. . . . . . . . . . . . . . 15 $\$
21		eqid 2622	. . . . . . . . . . . . . . . . 17 $\$ $\$
22	19	sseli 3599	. . . . . . . . . . . . . . . . 17 $\$
23	21, 22	fmpti 6383	. . . . . . . . . . . . . . . 16 $\$ $\$
24	23	a1i 11	. . . . . . . . . . . . . . 15 $\$ $\$
25		eqid 2622	. . . . . . . . . . . . . . . . 17 $\$ $\$
26		2re 11090	. . . . . . . . . . . . . . . . . . 19
27	26	a1i 11	. . . . . . . . . . . . . . . . . 18 $\$
28	22	rehalfcld 11279	. . . . . . . . . . . . . . . . . . 19 $\$
29	28	resincld 14873	. . . . . . . . . . . . . . . . . 18 $\$
30	27, 29	remulcld 10070	. . . . . . . . . . . . . . . . 17 $\$
31	25, 30	fmpti 6383	. . . . . . . . . . . . . . . 16 $\$ $\$
32	31	a1i 11	. . . . . . . . . . . . . . 15 $\$ $\$
33		iooretop 22569	. . . . . . . . . . . . . . . 16
34	33	a1i 11	. . . . . . . . . . . . . . 15
35		0re 10040	. . . . . . . . . . . . . . . . 17
36		negpilt0 39492	. . . . . . . . . . . . . . . . 17
37		pipos 24212	. . . . . . . . . . . . . . . . 17
38		pire 24210	. . . . . . . . . . . . . . . . . . . 20
39	38	renegcli 10342	. . . . . . . . . . . . . . . . . . 19
40	39	rexri 10097	. . . . . . . . . . . . . . . . . 18
41	38	rexri 10097	. . . . . . . . . . . . . . . . . 18
42		elioo2 12216	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
43	40, 41, 42	mp2an 708	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
44	35, 36, 37, 43	mpbir3an 1244	. . . . . . . . . . . . . . . 16
45	44	a1i 11	. . . . . . . . . . . . . . 15
46		eqid 2622	. . . . . . . . . . . . . . 15 $\$ $\$
47		1ex 10035	. . . . . . . . . . . . . . . . . . 19
48		eqid 2622	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
49	47, 48	dmmpti 6023	. . . . . . . . . . . . . . . . . 18 $\$ $\$
50		reelprrecn 10028	. . . . . . . . . . . . . . . . . . . . . . 23
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
52	12	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . 23
53	52	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
54		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
55	51	dvmptid 23720	. . . . . . . . . . . . . . . . . . . . . 22
56		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ℂ_fld
57	56	tgioo2 22606	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
58		sncldre 39208	. . . . . . . . . . . . . . . . . . . . . . . . 25
59	35, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
60		retopon 22567	. . . . . . . . . . . . . . . . . . . . . . . . . 26 TopOn
61	60	toponunii 20721	. . . . . . . . . . . . . . . . . . . . . . . . 25
62	61	difopn 20838	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
63	33, 59, 62	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $\$
65	51, 53, 54, 55, 20, 57, 56, 64	dvmptres 23726	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
66	65	trud 1493	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
67	66	eqcomi 2631	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
68	67	dmeqi 5325	. . . . . . . . . . . . . . . . . 18 $\$ $\$
69	49, 68	eqtr3i 2646	. . . . . . . . . . . . . . . . 17 $\$ $\$
70	69	eqimssi 3659	. . . . . . . . . . . . . . . 16 $\$ $\$
71	70	a1i 11	. . . . . . . . . . . . . . 15 $\$ $\$
72		fvex 6201	. . . . . . . . . . . . . . . . . . 19
73		eqid 2622	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
74	72, 73	dmmpti 6023	. . . . . . . . . . . . . . . . . 18 $\$ $\$
75		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
76	53	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
77	76	sincld 14860	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
78	75, 77	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	76	coscld 14861	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
80		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
81		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
83	52, 80, 82	divrec2d 10805	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
84	83	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
85	84	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . 26
86	85	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . 25
87	86	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . 24
88		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	12, 88	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
90	89	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . 26
91	90	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . 25
92		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
93		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94		halfcn 11247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	95, 96	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98	97	sincld 14860	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
99	93, 98	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
100	92, 99	fmpti 6383	. . . . . . . . . . . . . . . . . . . . . . . . . 26
101		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
103	102, 94	mulcli 10045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	97	coscld 14861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
106	104, 105	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107	106	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
108	101, 107	dmmptd 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109	108	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110	12, 109	sseqtr4i 3638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
111		dvasinbx 40135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
112	102, 94, 111	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
113	112	dmeqi 5325	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
114	110, 113	sseqtr4i 3638	. . . . . . . . . . . . . . . . . . . . . . . . . 26
115		dvcnre 40130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
116	100, 114, 115	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . 25
117	112	reseq1i 5392	. . . . . . . . . . . . . . . . . . . . . . . . . 26
118		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
119	12, 118	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26
120	102, 81	recidi 10756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
122	83	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
123	122	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124	121, 123	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125	52	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
126	125	coscld 14861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
127	126	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	124, 127	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	128	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	117, 119, 129	3eqtri 2648	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	91, 116, 130	3eqtri 2648	. . . . . . . . . . . . . . . . . . . . . . . 24
132	87, 131	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
134	51, 78, 79, 133, 20, 57, 56, 64	dvmptres 23726	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
135	134	trud 1493	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
136	135	eqcomi 2631	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
137	136	dmeqi 5325	. . . . . . . . . . . . . . . . . 18 $\$ $\$
138	74, 137	eqtr3i 2646	. . . . . . . . . . . . . . . . 17 $\$ $\$
139	138	eqimssi 3659	. . . . . . . . . . . . . . . 16 $\$ $\$
140	139	a1i 11	. . . . . . . . . . . . . . 15 $\$ $\$
141	17	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24
142	141	ssriv 3607	. . . . . . . . . . . . . . . . . . . . . . 23
143	142	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
144		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . 23
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
146	143, 145	idcncfg 40085	. . . . . . . . . . . . . . . . . . . . 21
147	146	trud 1493	. . . . . . . . . . . . . . . . . . . 20
148		cnlimc 23652	. . . . . . . . . . . . . . . . . . . . 21 $/\$ lim
149	142, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $/\$ lim
150	147, 149	mpbi 220	. . . . . . . . . . . . . . . . . . 19 $/\$ lim
151	150	simpri 478	. . . . . . . . . . . . . . . . . 18 lim
152		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
153		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 lim lim
154	152, 153	eleq12d 2695	. . . . . . . . . . . . . . . . . . 19 lim lim
155	154	rspccva 3308	. . . . . . . . . . . . . . . . . 18 lim $/\$ lim
156	151, 44, 155	mp2an 708	. . . . . . . . . . . . . . . . 17 lim
157		id 22	. . . . . . . . . . . . . . . . . . 19
158		eqid 2622	. . . . . . . . . . . . . . . . . . 19
159		c0ex 10034	. . . . . . . . . . . . . . . . . . 19
160	157, 158, 159	fvmpt 6282	. . . . . . . . . . . . . . . . . 18
161	44, 160	ax-mp 5	. . . . . . . . . . . . . . . . 17
162		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . 23
163	162	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22
164	158, 163	fmpti 6383	. . . . . . . . . . . . . . . . . . . . 21
165	164	a1i 11	. . . . . . . . . . . . . . . . . . . 20
166	165	limcdif 23640	. . . . . . . . . . . . . . . . . . 19 lim $\$ lim
167	166	trud 1493	. . . . . . . . . . . . . . . . . 18 lim $\$ lim
168		resmpt 5449	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
169	16, 168	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
170	169	oveq1i 6660	. . . . . . . . . . . . . . . . . 18 $\$ lim $\$ lim
171	167, 170	eqtri 2644	. . . . . . . . . . . . . . . . 17 lim $\$ lim
172	156, 161, 171	3eltr3i 2713	. . . . . . . . . . . . . . . 16 $\$ lim
173	172	a1i 11	. . . . . . . . . . . . . . 15 $\$ lim
174		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23
175	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
176		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . 25
177	175, 176, 175	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . . . 24
178	102, 177	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23
179		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
180	174, 178, 143, 145, 179	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . . . . 22
181		sincn 24198	. . . . . . . . . . . . . . . . . . . . . . . 24
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
183		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
184	183	divccncf 22709	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
185	102, 81, 184	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . 25
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
187	163	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
188	187	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
189	183, 186, 143, 145, 188	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . . . . . 23
190	182, 189	cncfmpt1f 22716	. . . . . . . . . . . . . . . . . . . . . 22
191	180, 190	mulcncf 23215	. . . . . . . . . . . . . . . . . . . . 21
192	191	trud 1493	. . . . . . . . . . . . . . . . . . . 20
193		cnlimc 23652	. . . . . . . . . . . . . . . . . . . . 21 $/\$ lim
194	142, 193	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $/\$ lim
195	192, 194	mpbi 220	. . . . . . . . . . . . . . . . . . 19 $/\$ lim
196	195	simpri 478	. . . . . . . . . . . . . . . . . 18 lim
197		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
198		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 lim lim
199	197, 198	eleq12d 2695	. . . . . . . . . . . . . . . . . . 19 lim lim
200	199	rspccva 3308	. . . . . . . . . . . . . . . . . 18 lim $/\$ lim
201	196, 44, 200	mp2an 708	. . . . . . . . . . . . . . . . 17 lim
202		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
203	102, 81	div0i 10759	. . . . . . . . . . . . . . . . . . . . . . . 24
204	202, 203	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
205	204	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
206		sin0 14879	. . . . . . . . . . . . . . . . . . . . . 22
207	205, 206	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21
208	207	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
209		2t0e0 11183	. . . . . . . . . . . . . . . . . . . 20
210	208, 209	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19
211		eqid 2622	. . . . . . . . . . . . . . . . . . 19
212	210, 211, 159	fvmpt 6282	. . . . . . . . . . . . . . . . . 18
213	44, 212	ax-mp 5	. . . . . . . . . . . . . . . . 17
214		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . 23
215	163	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . 24
216	215	sincld 14860	. . . . . . . . . . . . . . . . . . . . . . 23
217	214, 216	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . 22
218	211, 217	fmpti 6383	. . . . . . . . . . . . . . . . . . . . 21
219	218	a1i 11	. . . . . . . . . . . . . . . . . . . 20
220	219	limcdif 23640	. . . . . . . . . . . . . . . . . . 19 lim $\$ lim
221	220	trud 1493	. . . . . . . . . . . . . . . . . 18 lim $\$ lim
222		resmpt 5449	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
223	16, 222	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
224	223	oveq1i 6660	. . . . . . . . . . . . . . . . . 18 $\$ lim $\$ lim
225	221, 224	eqtri 2644	. . . . . . . . . . . . . . . . 17 lim $\$ lim
226	201, 213, 225	3eltr3i 2713	. . . . . . . . . . . . . . . 16 $\$ lim
227	226	a1i 11	. . . . . . . . . . . . . . 15 $\$ lim
228		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
229		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
230	229	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
231	230	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22
232	231	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
233		id 22	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
234	26	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $\$
235	19	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
236	235	rehalfcld 11279	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
237	236	resincld 14873	. . . . . . . . . . . . . . . . . . . . . 22 $\$
238	234, 237	remulcld 10070	. . . . . . . . . . . . . . . . . . . . 21 $\$
239	228, 232, 233, 238	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
240		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21 $\$
241	237	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 $\$
242	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $\$
243		ioossicc 12259	. . . . . . . . . . . . . . . . . . . . . . 23
244		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
245	243, 244	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 $\$
246		eldifsni 4320	. . . . . . . . . . . . . . . . . . . . . 22 $\$
247		fourierdlem44 40368	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
248	245, 246, 247	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $\$
249	240, 241, 242, 248	mulne0d 10679	. . . . . . . . . . . . . . . . . . . 20 $\$
250	239, 249	eqnetrd 2861	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
251	250	neneqd 2799	. . . . . . . . . . . . . . . . . 18 $\$ $\$
252	251	nrex 3000	. . . . . . . . . . . . . . . . 17 $\$ $\$
253	25	fnmpt 6020	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
254	253, 30	mprg 2926	. . . . . . . . . . . . . . . . . 18 $\$ $\$
255		ssid 3624	. . . . . . . . . . . . . . . . . 18 $\$ $\$
256		fvelimab 6253	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
257	254, 255, 256	mp2an 708	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
258	252, 257	mtbir 313	. . . . . . . . . . . . . . . 16 $\$ $\$
259	258	a1i 11	. . . . . . . . . . . . . . 15 $\$ $\$
260		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
261	229	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
262	261	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
263	235	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
264	263	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
265	264	coscld 14861	. . . . . . . . . . . . . . . . . . . . . 22 $\$
266	260, 262, 233, 265	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
267	236	rered 13964	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
268		halfpire 24216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	268	renegcli 10342	. . . . . . . . . . . . . . . . . . . . . . . . . 26
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
271	270	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
272	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
273	272	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
274		picn 24211	. . . . . . . . . . . . . . . . . . . . . . . . . 26
275		divneg 10719	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
276	274, 102, 81, 275	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . 25
277	39	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
278		2rp 11837	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
279	278	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
280	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
281	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
282		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
283	280, 281, 244, 282	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
284	277, 235, 279, 283	ltdiv1dd 11929	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
285	276, 284	syl5eqbr 4688	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
286	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
287		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
288	280, 281, 244, 287	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
289	235, 286, 279, 288	ltdiv1dd 11929	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
290	271, 273, 236, 285, 289	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
291	267, 290	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 $\$
292		cosne0 24276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
293	264, 291, 292	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $\$
294	266, 293	eqnetrd 2861	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
295	294	neneqd 2799	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
296	295	nrex 3000	. . . . . . . . . . . . . . . . . 18 $\$ $\$
297	72, 73	fnmpti 6022	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
298		fvelimab 6253	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
299	297, 255, 298	mp2an 708	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$
300	296, 299	mtbir 313	. . . . . . . . . . . . . . . . 17 $\$ $\$
301	135	imaeq1i 5463	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$
302	301	eleq2i 2693	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
303	300, 302	mtbir 313	. . . . . . . . . . . . . . . 16 $\$ $\$
304	303	a1i 11	. . . . . . . . . . . . . . 15 $\$ $\$
305		eqid 2622	. . . . . . . . . . . . . . . . 17 $\$ $\$
306		eqid 2622	. . . . . . . . . . . . . . . . 17 $\$ $\$
307	19	sseli 3599	. . . . . . . . . . . . . . . . . . . . . 22 $\$
308	307	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 $\$
309	308	halfcld 11277	. . . . . . . . . . . . . . . . . . . 20 $\$
310	309	coscld 14861	. . . . . . . . . . . . . . . . . . 19 $\$
311	307	rehalfcld 11279	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
312	311	rered 13964	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
313	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
314	313	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
315	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
316	315	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
317	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
318	317	renegcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
319	278	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
320	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
321	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
322		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
323		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
324	320, 321, 322, 323	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
325	318, 307, 319, 324	ltdiv1dd 11929	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
326	276, 325	syl5eqbr 4688	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
327		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
328	320, 321, 322, 327	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
329	307, 317, 319, 328	ltdiv1dd 11929	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
330	314, 316, 311, 326, 329	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
331	312, 330	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 $\$
332		cosne0 24276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
333	309, 331, 332	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $\$
334	333	neneqd 2799	. . . . . . . . . . . . . . . . . . . 20 $\$
335	311	recoscld 14874	. . . . . . . . . . . . . . . . . . . . 21 $\$
336		elsng 4191	. . . . . . . . . . . . . . . . . . . . 21
337	335, 336	syl 17	. . . . . . . . . . . . . . . . . . . 20 $\$
338	334, 337	mtbird 315	. . . . . . . . . . . . . . . . . . 19 $\$
339	310, 338	eldifd 3585	. . . . . . . . . . . . . . . . . 18 $\$ $\$
340	339	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$
341	309	ad2antrl 764	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
342		cosf 14855	. . . . . . . . . . . . . . . . . . . 20
343	342	a1i 11	. . . . . . . . . . . . . . . . . . 19
344	343	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 $/\$
345		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21
346	345	divccncf 22709	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
347	102, 81, 346	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22
348	347	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
349	141	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
350	349	halfcld 11277	. . . . . . . . . . . . . . . . . . . . 21 $/\$
351	345, 348, 143, 145, 350	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . . 20
352		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21
353	352, 203	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
354	351, 45, 353	cnmptlimc 23654	. . . . . . . . . . . . . . . . . . 19 lim
355		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
356	141	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . 24
357	355, 356	fmpti 6383	. . . . . . . . . . . . . . . . . . . . . . 23
358	357	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
359	358	limcdif 23640	. . . . . . . . . . . . . . . . . . . . 21 lim $\$ lim
360	359	trud 1493	. . . . . . . . . . . . . . . . . . . 20 lim $\$ lim
361		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
362	16, 361	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
363	362	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20 $\$ lim $\$ lim
364	360, 363	eqtri 2644	. . . . . . . . . . . . . . . . . . 19 lim $\$ lim
365	354, 364	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18 $\$ lim
366		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . 23
367	342, 366	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
368		dffn5 6241	. . . . . . . . . . . . . . . . . . . . . 22
369	367, 368	mpbi 220	. . . . . . . . . . . . . . . . . . . . 21
370		coscn 24199	. . . . . . . . . . . . . . . . . . . . 21
371	369, 370	eqeltrri 2698	. . . . . . . . . . . . . . . . . . . 20
372	371	a1i 11	. . . . . . . . . . . . . . . . . . 19
373		0cnd 10033	. . . . . . . . . . . . . . . . . . 19
374		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
375		cos0 14880	. . . . . . . . . . . . . . . . . . . 20
376	374, 375	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19
377	372, 373, 376	cnmptlimc 23654	. . . . . . . . . . . . . . . . . 18 lim
378		fveq2 6191	. . . . . . . . . . . . . . . . . 18
379		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
380	379, 375	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19
381	380	ad2antll 765	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$
382	341, 344, 365, 377, 378, 381	limcco 23657	. . . . . . . . . . . . . . . . 17 $\$ lim
383		ax-1ne0 10005	. . . . . . . . . . . . . . . . . 18
384	383	a1i 11	. . . . . . . . . . . . . . . . 17
385	305, 306, 340, 382, 384	reclimc 39885	. . . . . . . . . . . . . . . 16 $\$ lim
386		1div1e1 10717	. . . . . . . . . . . . . . . 16
387	66	fveq1i 6192	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
388		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
389		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
390		id 22	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
391		1red 10055	. . . . . . . . . . . . . . . . . . . . 21 $\$
392	388, 389, 390, 391	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
393	387, 392	syl5req 2669	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
394	135	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
395		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23
396	395	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
397	396	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
398	394, 397, 390, 335	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
399	398	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
400	393, 399	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
401	400	mpteq2ia 4740	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
402	401	oveq1i 6660	. . . . . . . . . . . . . . . 16 $\$ lim $\$ $\$ $\$ lim
403	385, 386, 402	3eltr3g 2717	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ lim
404	20, 24, 32, 34, 45, 46, 71, 140, 173, 227, 259, 304, 403	lhop 23779	. . . . . . . . . . . . . 14 $\$ $\$ $\$ lim
405	404	trud 1493	. . . . . . . . . . . . 13 $\$ $\$ $\$ lim
406		eqidd 2623	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
407		simpr 477	. . . . . . . . . . . . . . . . 17 $\$ $/\$
408	406, 407, 390, 307	fvmptd 6288	. . . . . . . . . . . . . . . 16 $\$ $\$
409		eqidd 2623	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
410	407	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
411	410	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
412	411	oveq2d 6666	. . . . . . . . . . . . . . . . 17 $\$ $/\$
413	26	a1i 11	. . . . . . . . . . . . . . . . . 18 $\$
414	311	resincld 14873	. . . . . . . . . . . . . . . . . 18 $\$
415	413, 414	remulcld 10070	. . . . . . . . . . . . . . . . 17 $\$
416	409, 412, 390, 415	fvmptd 6288	. . . . . . . . . . . . . . . 16 $\$ $\$
417	408, 416	oveq12d 6668	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
418	417	mpteq2ia 4740	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$
419	418	oveq1i 6660	. . . . . . . . . . . . 13 $\$ $\$ $\$ lim $\$ lim
420	405, 419	eleqtri 2699	. . . . . . . . . . . 12 $\$ lim
421	10	oveq1i 6660	. . . . . . . . . . . . . 14 lim lim
422	10	feq1i 6036	. . . . . . . . . . . . . . . . . . 19
423	14, 422	mpbi 220	. . . . . . . . . . . . . . . . . 18
424	423	a1i 11	. . . . . . . . . . . . . . . . 17
425	243	a1i 11	. . . . . . . . . . . . . . . . 17
426		iccssre 12255	. . . . . . . . . . . . . . . . . . . 20 $/\$
427	39, 38, 426	mp2an 708	. . . . . . . . . . . . . . . . . . 19
428	427	a1i 11	. . . . . . . . . . . . . . . . . 18
429	428, 12	syl6ss 3615	. . . . . . . . . . . . . . . . 17
430		eqid 2622	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t ℂ_fld ↾_t
431	39, 35, 36	ltleii 10160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
432	35, 38, 37	ltleii 10160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
433	39, 38	elicc2i 12239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
434	35, 431, 432, 433	mpbir3an 1244	. . . . . . . . . . . . . . . . . . . . . . . . . 26
435	159	snss 4316	. . . . . . . . . . . . . . . . . . . . . . . . . 26
436	434, 435	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . 25
437		ssequn2 3786	. . . . . . . . . . . . . . . . . . . . . . . . 25
438	436, 437	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . 24
439	438	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t ℂ_fld ↾_t
440		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25
441	56, 440	tgiooss 39733	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
442	427, 441	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t ↾_t
443	439, 442	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t ↾_t
444	443	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld ↾_t ↾_t
445	159	snss 4316	. . . . . . . . . . . . . . . . . . . . . . 23
446	44, 445	mpbi 220	. . . . . . . . . . . . . . . . . . . . . 22
447		ssequn2 3786	. . . . . . . . . . . . . . . . . . . . . 22
448	446, 447	mpbi 220	. . . . . . . . . . . . . . . . . . . . 21
449	444, 448	fveq12i 6196	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld ↾_t ↾_t
450		resttopon 20965	. . . . . . . . . . . . . . . . . . . . . . 23 TopOn $/\$ ↾_t TopOn
451	60, 427, 450	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 ↾_t TopOn
452	451	topontopi 20720	. . . . . . . . . . . . . . . . . . . . 21 ↾_t
453		retop 22565	. . . . . . . . . . . . . . . . . . . . . . . 24
454		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . 24
455	453, 454	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
456		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . . 24
457	33, 243, 456	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
458		restopnb 20979	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ ↾_t
459	455, 457, 458	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 ↾_t
460	33, 459	mpbi 220	. . . . . . . . . . . . . . . . . . . . 21 ↾_t
461		isopn3i 20886	. . . . . . . . . . . . . . . . . . . . 21 ↾_t $/\$ ↾_t ↾_t
462	452, 460, 461	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 ↾_t
463		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
464	449, 462, 463	3eqtrri 2649	. . . . . . . . . . . . . . . . . . 19 ℂ_fld ↾_t
465	44, 464	eleqtri 2699	. . . . . . . . . . . . . . . . . 18 ℂ_fld ↾_t
466	465	a1i 11	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t
467	424, 425, 429, 56, 430, 466	limcres 23650	. . . . . . . . . . . . . . . 16 lim lim
468	467	trud 1493	. . . . . . . . . . . . . . 15 lim lim
469	468	eqcomi 2631	. . . . . . . . . . . . . 14 lim lim
470		resmpt 5449	. . . . . . . . . . . . . . . 16
471	243, 470	ax-mp 5	. . . . . . . . . . . . . . 15
472	471	oveq1i 6660	. . . . . . . . . . . . . 14 lim lim
473	421, 469, 472	3eqtri 2648	. . . . . . . . . . . . 13 lim lim
474		eqid 2622	. . . . . . . . . . . . . . . . 17
475		iftrue 4092	. . . . . . . . . . . . . . . . . . . 20
476		1cnd 10056	. . . . . . . . . . . . . . . . . . . 20
477	475, 476	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19
478	477	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
479		iffalse 4095	. . . . . . . . . . . . . . . . . . . 20
480	479	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
481	141	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
482		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21 $/\$
483	481	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
484	483	sincld 14860	. . . . . . . . . . . . . . . . . . . . 21 $/\$
485	482, 484	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 $/\$
486	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
487	243	sseli 3599	. . . . . . . . . . . . . . . . . . . . . 22
488		neqne 2802	. . . . . . . . . . . . . . . . . . . . . 22
489		fourierdlem44 40368	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
490	487, 488, 489	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$
491	482, 484, 486, 490	mulne0d 10679	. . . . . . . . . . . . . . . . . . . 20 $/\$
492	481, 485, 491	divcld 10801	. . . . . . . . . . . . . . . . . . 19 $/\$
493	480, 492	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 $/\$
494	478, 493	pm2.61dan 832	. . . . . . . . . . . . . . . . 17
495	474, 494	fmpti 6383	. . . . . . . . . . . . . . . 16
496	495	a1i 11	. . . . . . . . . . . . . . 15
497	496	limcdif 23640	. . . . . . . . . . . . . 14 lim $\$ lim
498	497	trud 1493	. . . . . . . . . . . . 13 lim $\$ lim
499		resmpt 5449	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
500	16, 499	ax-mp 5	. . . . . . . . . . . . . . 15 $\$ $\$
501		eldifn 3733	. . . . . . . . . . . . . . . . . 18 $\$
502		velsn 4193	. . . . . . . . . . . . . . . . . 18
503	501, 502	sylnib 318	. . . . . . . . . . . . . . . . 17 $\$
504	503, 479	syl 17	. . . . . . . . . . . . . . . 16 $\$
505	504	mpteq2ia 4740	. . . . . . . . . . . . . . 15 $\$ $\$
506	500, 505	eqtri 2644	. . . . . . . . . . . . . 14 $\$ $\$
507	506	oveq1i 6660	. . . . . . . . . . . . 13 $\$ lim $\$ lim
508	473, 498, 507	3eqtrri 2649	. . . . . . . . . . . 12 $\$ lim lim
509	420, 508	eleqtri 2699	. . . . . . . . . . 11 lim
510	509	a1i 11	. . . . . . . . . 10 lim
511		fveq2 6191	. . . . . . . . . . 11
512	475, 10, 47	fvmpt 6282	. . . . . . . . . . . 12
513	434, 512	ax-mp 5	. . . . . . . . . . 11
514	511, 513	syl6eq 2672	. . . . . . . . . 10
515		oveq2 6658	. . . . . . . . . 10 lim lim
516	510, 514, 515	3eltr4d 2716	. . . . . . . . 9 lim
517	427, 12	sstri 3612	. . . . . . . . . . 11
518	517	a1i 11	. . . . . . . . . 10
519	38	a1i 11	. . . . . . . . . . . 12
520	519	renegcld 10457	. . . . . . . . . . 11
521		id 22	. . . . . . . . . . . 12
522	35	a1i 11	. . . . . . . . . . . 12
523	521, 522	eqeltrd 2701	. . . . . . . . . . 11
524	431, 521	syl5breqr 4691	. . . . . . . . . . 11
525	521, 432	syl6eqbr 4692	. . . . . . . . . . 11
526	520, 519, 523, 524, 525	eliccd 39726	. . . . . . . . . 10
527	57	oveq1i 6660	. . . . . . . . . . . 12 ↾_t ℂ_fld ↾_t ↾_t
528	56	cnfldtop 22587	. . . . . . . . . . . . 13 ℂ_fld
529		reex 10027	. . . . . . . . . . . . 13
530		restabs 20969	. . . . . . . . . . . . 13 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
531	528, 427, 529, 530	mp3an 1424	. . . . . . . . . . . 12 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
532	527, 531	eqtri 2644	. . . . . . . . . . 11 ↾_t ℂ_fld ↾_t
533	56, 532	cnplimc 23651	. . . . . . . . . 10 $/\$ ↾_t ℂ_fld $/\$ lim
534	518, 526, 533	syl2anc 693	. . . . . . . . 9 ↾_t ℂ_fld $/\$ lim
535	15, 516, 534	mpbir2and 957	. . . . . . . 8 ↾_t ℂ_fld
536	535	adantl 482	. . . . . . 7 $/\$ ↾_t ℂ_fld
537		simpl 473	. . . . . . . . . . 11 $/\$
538	502	notbii 310	. . . . . . . . . . . . 13
539	538	biimpri 218	. . . . . . . . . . . 12
540	539	adantl 482	. . . . . . . . . . 11 $/\$
541	537, 540	eldifd 3585	. . . . . . . . . 10 $/\$ $\$
542		fveq2 6191	. . . . . . . . . . . 12 ↾_t $\$ ℂ_fld ↾_t $\$ ℂ_fld
543	542	eleq2d 2687	. . . . . . . . . . 11 $\$ ↾_t $\$ ℂ_fld $\$ ↾_t $\$ ℂ_fld
544	429	ssdifssd 3748	. . . . . . . . . . . . . . . . 17 $\$
545	544, 145	idcncfg 40085	. . . . . . . . . . . . . . . 16 $\$ $\$
546		eqid 2622	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
547		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21 $\$
548		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
549	517, 548	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
550	549	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . 22 $\$
551	550	sincld 14860	. . . . . . . . . . . . . . . . . . . . 21 $\$
552	547, 551	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 $\$
553	81	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
554		eldifsni 4320	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
555	548, 554, 489	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
556	547, 551, 553, 555	mulne0d 10679	. . . . . . . . . . . . . . . . . . . . . 22 $\$
557	556	neneqd 2799	. . . . . . . . . . . . . . . . . . . . 21 $\$
558		elsng 4191	. . . . . . . . . . . . . . . . . . . . . 22
559	552, 558	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $\$
560	557, 559	mtbird 315	. . . . . . . . . . . . . . . . . . . 20 $\$
561	552, 560	eldifd 3585	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
562	546, 561	fmpti 6383	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
563		difss 3737	. . . . . . . . . . . . . . . . . . 19 $\$
564		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
565	175, 176, 175	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . . 23
566	102, 565	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22
567		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$
568	564, 566, 544, 145, 567	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
569	549, 547, 553	divrecd 10804	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
570	569	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
571		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25
572	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
573		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
574	572, 573, 572	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . . . . . 26
575	94, 574	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . 25
576	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
577	571, 575, 544, 145, 576	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
578	545, 577	mulcncf 23215	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
579	570, 578	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
580	182, 579	cncfmpt1f 22716	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
581	568, 580	mulcncf 23215	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
582	581	trud 1493	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
583		cncffvrn 22701	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
584	563, 582, 583	mp2an 708	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$ $\$ $\$
585	562, 584	mpbir 221	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
586	585	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
587	545, 586	divcncf 23216	. . . . . . . . . . . . . . 15 $\$ $\$
588	587	trud 1493	. . . . . . . . . . . . . 14 $\$ $\$
589	428	ssdifssd 3748	. . . . . . . . . . . . . . . . 17 $\$
590	589	trud 1493	. . . . . . . . . . . . . . . 16 $\$
591	590, 12	sstri 3612	. . . . . . . . . . . . . . 15 $\$
592	57	oveq1i 6660	. . . . . . . . . . . . . . . . 17 ↾_t $\$ ℂ_fld ↾_t ↾_t $\$
593		restabs 20969	. . . . . . . . . . . . . . . . . 18 ℂ_fld $/\$ $\$ $/\$ ℂ_fld ↾_t ↾_t $\$ ℂ_fld ↾_t $\$
594	528, 590, 529, 593	mp3an 1424	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t ↾_t $\$ ℂ_fld ↾_t $\$
595	592, 594	eqtri 2644	. . . . . . . . . . . . . . . 16 ↾_t $\$ ℂ_fld ↾_t $\$
596		unicntop 22589	. . . . . . . . . . . . . . . . . . 19 ℂ_fld
597	596	restid 16094	. . . . . . . . . . . . . . . . . 18 ℂ_fld ℂ_fld ↾_t ℂ_fld
598	528, 597	ax-mp 5	. . . . . . . . . . . . . . . . 17 ℂ_fld ↾_t ℂ_fld
599	598	eqcomi 2631	. . . . . . . . . . . . . . . 16 ℂ_fld ℂ_fld ↾_t
600	56, 595, 599	cncfcn 22712	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ ↾_t $\$ ℂ_fld
601	591, 144, 600	mp2an 708	. . . . . . . . . . . . . 14 $\$ ↾_t $\$ ℂ_fld
602	588, 601	eleqtri 2699	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ℂ_fld
603		resttopon 20965	. . . . . . . . . . . . . . 15 TopOn $/\$ $\$ ↾_t $\$ TopOn $\$
604	60, 590, 603	mp2an 708	. . . . . . . . . . . . . 14 ↾_t $\$ TopOn $\$
605	56	cnfldtopon 22586	. . . . . . . . . . . . . 14 ℂ_fld TopOn
606		cncnp 21084	. . . . . . . . . . . . . 14 ↾_t $\$ TopOn $\$ $/\$ ℂ_fld TopOn $\$ ↾_t $\$ ℂ_fld $\$ $\$ $/\$ $\$ $\$ ↾_t $\$ ℂ_fld
607	604, 605, 606	mp2an 708	. . . . . . . . . . . . 13 $\$ ↾_t $\$ ℂ_fld $\$ $\$ $/\$ $\$ $\$ ↾_t $\$ ℂ_fld
608	602, 607	mpbi 220	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ ↾_t $\$ ℂ_fld
609	608	simpri 478	. . . . . . . . . . 11 $\$ $\$ ↾_t $\$ ℂ_fld
610	543, 609	vtoclri 3283	. . . . . . . . . 10 $\$ $\$ ↾_t $\$ ℂ_fld
611	541, 610	syl 17	. . . . . . . . 9 $/\$ $\$ ↾_t $\$ ℂ_fld
612	10	reseq1i 5392	. . . . . . . . . 10 $\$ $\$
613		difss 3737	. . . . . . . . . . 11 $\$
614		resmpt 5449	. . . . . . . . . . 11 $\$ $\$ $\$
615	613, 614	ax-mp 5	. . . . . . . . . 10 $\$ $\$
616		eldifn 3733	. . . . . . . . . . . . 13 $\$
617	616, 502	sylnib 318	. . . . . . . . . . . 12 $\$
618	617, 479	syl 17	. . . . . . . . . . 11 $\$
619	618	mpteq2ia 4740	. . . . . . . . . 10 $\$ $\$
620	612, 615, 619	3eqtri 2648	. . . . . . . . 9 $\$ $\$
621		restabs 20969	. . . . . . . . . . . 12 $/\$ $\$ $/\$ ↾_t ↾_t $\$ ↾_t $\$
622	453, 613, 454, 621	mp3an 1424	. . . . . . . . . . 11 ↾_t ↾_t $\$ ↾_t $\$
623	622	oveq1i 6660	. . . . . . . . . 10 ↾_t ↾_t $\$ ℂ_fld ↾_t $\$ ℂ_fld
624	623	fveq1i 6192	. . . . . . . . 9 ↾_t ↾_t $\$ ℂ_fld ↾_t $\$ ℂ_fld
625	611, 620, 624	3eltr4g 2718	. . . . . . . 8 $/\$ $\$ ↾_t ↾_t $\$ ℂ_fld
626	452, 613	pm3.2i 471	. . . . . . . . . 10 ↾_t $/\$ $\$
627	626	a1i 11	. . . . . . . . 9 $/\$ ↾_t $/\$ $\$
628		ssdif 3745	. . . . . . . . . . . . . 14 $\$ $\$
629	427, 628	ax-mp 5	. . . . . . . . . . . . 13 $\$ $\$
630	629, 541	sseldi 3601	. . . . . . . . . . . 12 $/\$ $\$
631		sscon 3744	. . . . . . . . . . . . . . . . 17 $\$ $\$
632	436, 631	ax-mp 5	. . . . . . . . . . . . . . . 16 $\$ $\$
633	629, 632	unssi 3788	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
634		simpr 477	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
635		eldifn 3733	. . . . . . . . . . . . . . . . . . . 20 $\$
636	635	adantr 481	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
637	634, 636	eldifd 3585	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$
638		elun1 3780	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
639	637, 638	syl 17	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$
640		eldifi 3732	. . . . . . . . . . . . . . . . . . . 20 $\$
641	640	adantr 481	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
642		simpr 477	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
643	641, 642	eldifd 3585	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$
644		elun2 3781	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
645	643, 644	syl 17	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$
646	639, 645	pm2.61dan 832	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
647	646	ssriv 3607	. . . . . . . . . . . . . . 15 $\$ $\$ $\$
648	633, 647	eqssi 3619	. . . . . . . . . . . . . 14 $\$ $\$ $\$
649	648	fveq2i 6194	. . . . . . . . . . . . 13 $\$ $\$ $\$
650	61	cldopn 20835	. . . . . . . . . . . . . . 15 $\$
651	59, 650	ax-mp 5	. . . . . . . . . . . . . 14 $\$
652		isopn3i 20886	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
653	453, 651, 652	mp2an 708	. . . . . . . . . . . . 13 $\$ $\$
654	649, 653	eqtri 2644	. . . . . . . . . . . 12 $\$ $\$ $\$
655	630, 654	syl6eleqr 2712	. . . . . . . . . . 11 $/\$ $\$ $\$
656	655, 537	elind 3798	. . . . . . . . . 10 $/\$ $\$ $\$
657		eqid 2622	. . . . . . . . . . . 12 ↾_t ↾_t
658	61, 657	restntr 20986	. . . . . . . . . . 11 $/\$ $/\$ $\$ ↾_t $\$ $\$ $\$
659	453, 427, 613, 658	mp3an 1424	. . . . . . . . . 10 ↾_t $\$ $\$ $\$
660	656, 659	syl6eleqr 2712	. . . . . . . . 9 $/\$ ↾_t $\$
661	14	a1i 11	. . . . . . . . 9 $/\$
662	451	toponunii 20721	. . . . . . . . . 10 ↾_t
663	662, 596	cnprest 21093	. . . . . . . . 9 ↾_t $/\$ $\$ $/\$ ↾_t $\$ $/\$ ↾_t ℂ_fld $\$ ↾_t ↾_t $\$ ℂ_fld
664	627, 660, 661, 663	syl12anc 1324	. . . . . . . 8 $/\$ ↾_t ℂ_fld $\$ ↾_t ↾_t $\$ ℂ_fld
665	625, 664	mpbird 247	. . . . . . 7 $/\$ ↾_t ℂ_fld
666	536, 665	pm2.61dan 832	. . . . . 6 ↾_t ℂ_fld
667	666	rgen 2922	. . . . 5 ↾_t ℂ_fld
668		cncnp 21084	. . . . . 6 ↾_t TopOn $/\$ ℂ_fld TopOn ↾_t ℂ_fld $/\$ ↾_t ℂ_fld
669	451, 605, 668	mp2an 708	. . . . 5 ↾_t ℂ_fld $/\$ ↾_t ℂ_fld
670	14, 667, 669	mpbir2an 955	. . . 4 ↾_t ℂ_fld
671	56, 532, 599	cncfcn 22712	. . . . . 6 $/\$ ↾_t ℂ_fld
672	517, 144, 671	mp2an 708	. . . . 5 ↾_t ℂ_fld
673	672	eqcomi 2631	. . . 4 ↾_t ℂ_fld
674	670, 673	eleqtri 2699	. . 3
675		cncffvrn 22701	. . 3 $/\$
676	12, 674, 675	mp2an 708	. 2
677	11, 676	mpbir 221	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wtru 1484

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

cif 4086

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

cres 5116

cima 5117

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

cmul 9941

cxr 10073

clt 10074

cle 10075

cneg 10267

cdiv 10684

c2 11070

crp 11832

cioo 12175

cicc 12178

cre 13837

csin 14794

ccos 14795

cpi 14797 ↾_t crest 16081

ctopn 16082

ctg 16098 ℂ_fldccnfld 19746

ctop 20698 TopOnctopon 20715

ccld 20820

cnt 20821

ccn 21028

ccnp 21029

ccncf 22679 lim

climc 23626

cdv 23627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-t1 21118 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631

This theorem is referenced by: fourierdlem77 40400 fourierdlem78 40401 fourierdlem85 40408 fourierdlem88 40411

W3C validator