dirkercncflem2 - Mathbox for Glauco Siliprandi

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

Theorem dirkercncflem2 40321

Description: Lemma used to prove that the Dirichlet Kernel is continuous at

points that are multiples of

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

**Hypotheses**
Ref	Expression
dirkercncflem2.d
dirkercncflem2.f	$\$
dirkercncflem2.g	$\$
dirkercncflem2.yne0	$/\$ $\$
dirkercncflem2.h	$\$
dirkercncflem2.i	$\$
dirkercncflem2.l
dirkercncflem2.n
dirkercncflem2.y
dirkercncflem2.ymod
dirkercncflem2.11	$/\$ $\$

**Assertion**
Ref	Expression
dirkercncflem2	$\$ lim

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem dirkercncflem2**
Step	Hyp	Ref	Expression
1		difss 3737	. . . . 5 $\$
2		ioossre 12235	. . . . 5
3	1, 2	sstri 3612	. . . 4 $\$
4	3	a1i 11	. . 3 $\$
5		dirkercncflem2.n	. . . . . . . . 9
6	5	adantr 481	. . . . . . . 8 $/\$ $\$
7	6	nnred 11035	. . . . . . 7 $/\$ $\$
8		halfre 11246	. . . . . . . 8
9	8	a1i 11	. . . . . . 7 $/\$ $\$
10	7, 9	readdcld 10069	. . . . . 6 $/\$ $\$
11	4	sselda 3603	. . . . . 6 $/\$ $\$
12	10, 11	remulcld 10070	. . . . 5 $/\$ $\$
13	12	resincld 14873	. . . 4 $/\$ $\$
14		dirkercncflem2.f	. . . 4 $\$
15	13, 14	fmptd 6385	. . 3 $\$
16		2re 11090	. . . . . . 7
17		pire 24210	. . . . . . 7
18	16, 17	remulcli 10054	. . . . . 6
19	18	a1i 11	. . . . 5 $/\$ $\$
20	11	rehalfcld 11279	. . . . . 6 $/\$ $\$
21	20	resincld 14873	. . . . 5 $/\$ $\$
22	19, 21	remulcld 10070	. . . 4 $/\$ $\$
23		dirkercncflem2.g	. . . 4 $\$
24	22, 23	fmptd 6385	. . 3 $\$
25		iooretop 22569	. . . 4
26	25	a1i 11	. . 3
27		dirkercncflem2.y	. . 3
28		eqid 2622	. . 3 $\$ $\$
29	14	a1i 11	. . . . . . . 8 $\$
30	29	oveq2d 6666	. . . . . . 7 $\$
31		resmpt 5449	. . . . . . . . . . . 12 $\$ $\$ $\$
32	3, 31	ax-mp 5	. . . . . . . . . . 11 $\$ $\$
33	32	eqcomi 2631	. . . . . . . . . 10 $\$ $\$
34	33	a1i 11	. . . . . . . . 9 $\$ $\$
35	34	oveq2d 6666	. . . . . . . 8 $\$ $\$
36		ax-resscn 9993	. . . . . . . . . 10
37	36	a1i 11	. . . . . . . . 9
38	5	nncnd 11036	. . . . . . . . . . . . . 14
39		halfcn 11247	. . . . . . . . . . . . . . 15
40	39	a1i 11	. . . . . . . . . . . . . 14
41	38, 40	addcld 10059	. . . . . . . . . . . . 13
42	41	adantr 481	. . . . . . . . . . . 12 $/\$
43	37	sselda 3603	. . . . . . . . . . . 12 $/\$
44	42, 43	mulcld 10060	. . . . . . . . . . 11 $/\$
45	44	sincld 14860	. . . . . . . . . 10 $/\$
46		eqid 2622	. . . . . . . . . 10
47	45, 46	fmptd 6385	. . . . . . . . 9
48		ssid 3624	. . . . . . . . . . 11
49	48, 3	pm3.2i 471	. . . . . . . . . 10 $/\$ $\$
50	49	a1i 11	. . . . . . . . 9 $/\$ $\$
51		eqid 2622	. . . . . . . . . 10 ℂ_fld ℂ_fld
52	51	tgioo2 22606	. . . . . . . . . 10 ℂ_fld ↾_t
53	51, 52	dvres 23675	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$ $\$ $\$
54	37, 47, 50, 53	syl21anc 1325	. . . . . . . 8 $\$ $\$
55		retop 22565	. . . . . . . . . . 11
56		rehaus 22602	. . . . . . . . . . . . 13
57	27	elioored 39776	. . . . . . . . . . . . 13
58		uniretop 22566	. . . . . . . . . . . . . 14
59	58	sncld 21175	. . . . . . . . . . . . 13 $/\$
60	56, 57, 59	sylancr 695	. . . . . . . . . . . 12
61	58	difopn 20838	. . . . . . . . . . . 12 $/\$ $\$
62	25, 60, 61	sylancr 695	. . . . . . . . . . 11 $\$
63		isopn3i 20886	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$
64	55, 62, 63	sylancr 695	. . . . . . . . . 10 $\$ $\$
65	64	reseq2d 5396	. . . . . . . . 9 $\$ $\$
66		reelprrecn 10028	. . . . . . . . . . . . 13
67	66	a1i 11	. . . . . . . . . . . 12
68	41	adantr 481	. . . . . . . . . . . . . . 15 $/\$
69		simpr 477	. . . . . . . . . . . . . . 15 $/\$
70	68, 69	mulcld 10060	. . . . . . . . . . . . . 14 $/\$
71	70	sincld 14860	. . . . . . . . . . . . 13 $/\$
72		eqid 2622	. . . . . . . . . . . . 13
73	71, 72	fmptd 6385	. . . . . . . . . . . 12
74		ssid 3624	. . . . . . . . . . . . 13
75	74	a1i 11	. . . . . . . . . . . 12
76		dvsinax 40127	. . . . . . . . . . . . . . . 16
77	41, 76	syl 17	. . . . . . . . . . . . . . 15
78	77	dmeqd 5326	. . . . . . . . . . . . . 14
79		eqid 2622	. . . . . . . . . . . . . . 15
80	70	coscld 14861	. . . . . . . . . . . . . . . 16 $/\$
81	68, 80	mulcld 10060	. . . . . . . . . . . . . . 15 $/\$
82	79, 81	dmmptd 6024	. . . . . . . . . . . . . 14
83	78, 82	eqtrd 2656	. . . . . . . . . . . . 13
84	36, 83	syl5sseqr 3654	. . . . . . . . . . . 12
85		dvres3 23677	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
86	67, 73, 75, 84, 85	syl22anc 1327	. . . . . . . . . . 11
87		resmpt 5449	. . . . . . . . . . . . 13
88	36, 87	mp1i 13	. . . . . . . . . . . 12
89	88	oveq2d 6666	. . . . . . . . . . 11
90	77	reseq1d 5395	. . . . . . . . . . . 12
91		resmpt 5449	. . . . . . . . . . . . 13
92	36, 91	ax-mp 5	. . . . . . . . . . . 12
93	90, 92	syl6eq 2672	. . . . . . . . . . 11
94	86, 89, 93	3eqtr3d 2664	. . . . . . . . . 10
95	94	reseq1d 5395	. . . . . . . . 9 $\$ $\$
96		resmpt 5449	. . . . . . . . . 10 $\$ $\$ $\$
97	3, 96	mp1i 13	. . . . . . . . 9 $\$ $\$
98	65, 95, 97	3eqtrd 2660	. . . . . . . 8 $\$ $\$
99	35, 54, 98	3eqtrd 2660	. . . . . . 7 $\$ $\$
100		dirkercncflem2.h	. . . . . . . . 9 $\$
101	100	a1i 11	. . . . . . . 8 $\$
102	101	eqcomd 2628	. . . . . . 7 $\$
103	30, 99, 102	3eqtrd 2660	. . . . . 6
104	103	dmeqd 5326	. . . . 5
105	11	recnd 10068	. . . . . . 7 $/\$ $\$
106	105, 81	syldan 487	. . . . . 6 $/\$ $\$
107	100, 106	dmmptd 6024	. . . . 5 $\$
108	104, 107	eqtr2d 2657	. . . 4 $\$
109		eqimss 3657	. . . 4 $\$ $\$
110	108, 109	syl 17	. . 3 $\$
111		dirkercncflem2.i	. . . . . . . 8 $\$
112	111	a1i 11	. . . . . . 7 $\$
113		resmpt 5449	. . . . . . . . . . . . 13 $\$ $\$ $\$
114	3, 113	ax-mp 5	. . . . . . . . . . . 12 $\$ $\$
115	114	eqcomi 2631	. . . . . . . . . . 11 $\$ $\$
116	115	oveq2i 6661	. . . . . . . . . 10 $\$ $\$
117	116	a1i 11	. . . . . . . . 9 $\$ $\$
118		2cn 11091	. . . . . . . . . . . . . 14
119		picn 24211	. . . . . . . . . . . . . 14
120	118, 119	mulcli 10045	. . . . . . . . . . . . 13
121	120	a1i 11	. . . . . . . . . . . 12 $/\$
122	43	halfcld 11277	. . . . . . . . . . . . 13 $/\$
123	122	sincld 14860	. . . . . . . . . . . 12 $/\$
124	121, 123	mulcld 10060	. . . . . . . . . . 11 $/\$
125		eqid 2622	. . . . . . . . . . 11
126	124, 125	fmptd 6385	. . . . . . . . . 10
127	51, 52	dvres 23675	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$ $\$
128	37, 126, 50, 127	syl21anc 1325	. . . . . . . . 9 $\$ $\$
129	64	reseq2d 5396	. . . . . . . . . 10 $\$ $\$
130	36	sseli 3599	. . . . . . . . . . . . . . . 16
131		1cnd 10056	. . . . . . . . . . . . . . . . . . . . 21
132		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21
133		id 22	. . . . . . . . . . . . . . . . . . . . 21
134		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . 22
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
136	131, 132, 133, 135	div13d 10825	. . . . . . . . . . . . . . . . . . . 20
137		halfcl 11257	. . . . . . . . . . . . . . . . . . . . 21
138	137	mulid1d 10057	. . . . . . . . . . . . . . . . . . . 20
139	136, 138	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19
140	139	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
141	140	oveq2d 6666	. . . . . . . . . . . . . . . . 17
142	141	eqcomd 2628	. . . . . . . . . . . . . . . 16
143	130, 142	syl 17	. . . . . . . . . . . . . . 15
144	143	adantl 482	. . . . . . . . . . . . . 14 $/\$
145	144	mpteq2dva 4744	. . . . . . . . . . . . 13
146	145	oveq2d 6666	. . . . . . . . . . . 12
147	120	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
148	39	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
149	148, 69	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$
150	149	sincld 14860	. . . . . . . . . . . . . . . . 17 $/\$
151	147, 150	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$
152		eqid 2622	. . . . . . . . . . . . . . . 16
153	151, 152	fmptd 6385	. . . . . . . . . . . . . . 15
154		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21
155	119	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
156	154, 155	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20
157		dvasinbx 40135	. . . . . . . . . . . . . . . . . . . 20 $/\$
158	156, 39, 157	sylancl 694	. . . . . . . . . . . . . . . . . . 19
159		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
160	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	159, 160, 148	mul32d 10246	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
162	134	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
163	159, 162	recidd 10796	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
164	163	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
165	160	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
166	161, 164, 165	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . 21 $/\$
167	139	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
168	167	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
169	166, 168	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 $/\$
170	169	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19
171	158, 170	eqtrd 2656	. . . . . . . . . . . . . . . . . 18
172	171	dmeqd 5326	. . . . . . . . . . . . . . . . 17
173		eqid 2622	. . . . . . . . . . . . . . . . . 18
174	69	halfcld 11277	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	174	coscld 14861	. . . . . . . . . . . . . . . . . . 19 $/\$
176	160, 175	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$
177	173, 176	dmmptd 6024	. . . . . . . . . . . . . . . . 17
178	172, 177	eqtrd 2656	. . . . . . . . . . . . . . . 16
179	36, 178	syl5sseqr 3654	. . . . . . . . . . . . . . 15
180		dvres3 23677	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
181	67, 153, 75, 179, 180	syl22anc 1327	. . . . . . . . . . . . . 14
182		resmpt 5449	. . . . . . . . . . . . . . . 16
183	36, 182	mp1i 13	. . . . . . . . . . . . . . 15
184	183	oveq2d 6666	. . . . . . . . . . . . . 14
185	171	reseq1d 5395	. . . . . . . . . . . . . 14
186	181, 184, 185	3eqtr3d 2664	. . . . . . . . . . . . 13
187		resmpt 5449	. . . . . . . . . . . . . 14
188	36, 187	ax-mp 5	. . . . . . . . . . . . 13
189	186, 188	syl6eq 2672	. . . . . . . . . . . 12
190	146, 189	eqtrd 2656	. . . . . . . . . . 11
191	190	reseq1d 5395	. . . . . . . . . 10 $\$ $\$
192	4	resmptd 5452	. . . . . . . . . 10 $\$ $\$
193	129, 191, 192	3eqtrd 2660	. . . . . . . . 9 $\$ $\$
194	117, 128, 193	3eqtrd 2660	. . . . . . . 8 $\$ $\$
195	194	eqcomd 2628	. . . . . . 7 $\$ $\$
196	23	a1i 11	. . . . . . . . 9 $\$
197	196	oveq2d 6666	. . . . . . . 8 $\$
198	197	eqcomd 2628	. . . . . . 7 $\$
199	112, 195, 198	3eqtrrd 2661	. . . . . 6
200	199	dmeqd 5326	. . . . 5
201	105, 176	syldan 487	. . . . . 6 $/\$ $\$
202	111, 201	dmmptd 6024	. . . . 5 $\$
203	200, 202	eqtr2d 2657	. . . 4 $\$
204		eqimss 3657	. . . 4 $\$ $\$
205	203, 204	syl 17	. . 3 $\$
206	105, 70	syldan 487	. . . . . . . 8 $/\$ $\$
207	206	ralrimiva 2966	. . . . . . 7 $\$
208		eqid 2622	. . . . . . . 8 $\$ $\$
209	208	fnmpt 6020	. . . . . . 7 $\$ $\$ $\$
210	207, 209	syl 17	. . . . . 6 $\$ $\$
211		eqidd 2623	. . . . . . . . . 10 $/\$ $\$ $\$ $\$
212		simpr 477	. . . . . . . . . . 11 $/\$ $\$ $/\$
213	212	oveq2d 6666	. . . . . . . . . 10 $/\$ $\$ $/\$
214		simpr 477	. . . . . . . . . 10 $/\$ $\$ $\$
215	38	adantr 481	. . . . . . . . . . . 12 $/\$ $\$
216		1cnd 10056	. . . . . . . . . . . . 13 $/\$ $\$
217	216	halfcld 11277	. . . . . . . . . . . 12 $/\$ $\$
218	215, 217	addcld 10059	. . . . . . . . . . 11 $/\$ $\$
219		eldifi 3732	. . . . . . . . . . . . . 14 $\$
220	219	elioored 39776	. . . . . . . . . . . . 13 $\$
221	220	recnd 10068	. . . . . . . . . . . 12 $\$
222	221	adantl 482	. . . . . . . . . . 11 $/\$ $\$
223	218, 222	mulcld 10060	. . . . . . . . . 10 $/\$ $\$
224	211, 213, 214, 223	fvmptd 6288	. . . . . . . . 9 $/\$ $\$ $\$
225		eleq1 2689	. . . . . . . . . . . . . . . 16 $\$ $\$
226	225	anbi2d 740	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$
227		oveq1 6657	. . . . . . . . . . . . . . . 16
228	227	neeq1d 2853	. . . . . . . . . . . . . . 15
229	226, 228	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$
230		eldifi 3732	. . . . . . . . . . . . . . . . . . . . 21 $\$
231		elioore 12205	. . . . . . . . . . . . . . . . . . . . 21
232	230, 231, 130	3syl 18	. . . . . . . . . . . . . . . . . . . 20 $\$
233		2cnd 11093	. . . . . . . . . . . . . . . . . . . 20 $\$
234	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $\$
235	134	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $\$
236		0re 10040	. . . . . . . . . . . . . . . . . . . . . 22
237		pipos 24212	. . . . . . . . . . . . . . . . . . . . . 22
238	236, 237	gtneii 10149	. . . . . . . . . . . . . . . . . . . . 21
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $\$
240	232, 233, 234, 235, 239	divdiv1d 10832	. . . . . . . . . . . . . . . . . . 19 $\$
241	240	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 $\$
242	241	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $\$
243		dirkercncflem2.yne0	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
244	243	neneqd 2799	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
245	105	halfcld 11277	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
246		sineq0 24273	. . . . . . . . . . . . . . . . . . 19
247	245, 246	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
248	244, 247	mtbid 314	. . . . . . . . . . . . . . . . 17 $/\$ $\$
249	242, 248	eqneltrd 2720	. . . . . . . . . . . . . . . 16 $/\$ $\$
250		2rp 11837	. . . . . . . . . . . . . . . . . 18
251		pirp 24213	. . . . . . . . . . . . . . . . . 18
252		rpmulcl 11855	. . . . . . . . . . . . . . . . . 18 $/\$
253	250, 251, 252	mp2an 708	. . . . . . . . . . . . . . . . 17
254		mod0 12675	. . . . . . . . . . . . . . . . 17 $/\$
255	11, 253, 254	sylancl 694	. . . . . . . . . . . . . . . 16 $/\$ $\$
256	249, 255	mtbird 315	. . . . . . . . . . . . . . 15 $/\$ $\$
257	256	neqned 2801	. . . . . . . . . . . . . 14 $/\$ $\$
258	229, 257	chvarv 2263	. . . . . . . . . . . . 13 $/\$ $\$
259	258	neneqd 2799	. . . . . . . . . . . 12 $/\$ $\$
260		simpll 790	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
261		simpr 477	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$
262	221	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$
263	57	recnd 10068	. . . . . . . . . . . . . . . 16
264	263	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$
265		0red 10041	. . . . . . . . . . . . . . . . . . 19
266	5	nnred 11035	. . . . . . . . . . . . . . . . . . 19
267		1red 10055	. . . . . . . . . . . . . . . . . . . . 21
268	267	rehalfcld 11279	. . . . . . . . . . . . . . . . . . . 20
269	266, 268	readdcld 10069	. . . . . . . . . . . . . . . . . . 19
270	5	nngt0d 11064	. . . . . . . . . . . . . . . . . . 19
271	250	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
272	271	rpreccld 11882	. . . . . . . . . . . . . . . . . . . 20
273	266, 272	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . 19
274	265, 266, 269, 270, 273	lttrd 10198	. . . . . . . . . . . . . . . . . 18
275	274	gt0ne0d 10592	. . . . . . . . . . . . . . . . 17
276	41, 275	jca 554	. . . . . . . . . . . . . . . 16 $/\$
277	276	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $/\$
278		mulcan 10664	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
279	262, 264, 277, 278	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$
280	261, 279	mpbid 222	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
281		oveq1 6657	. . . . . . . . . . . . . 14
282		dirkercncflem2.ymod	. . . . . . . . . . . . . 14
283	281, 282	sylan9eqr 2678	. . . . . . . . . . . . 13 $/\$
284	260, 280, 283	syl2anc 693	. . . . . . . . . . . 12 $/\$ $\$ $/\$
285	259, 284	mtand 691	. . . . . . . . . . 11 $/\$ $\$
286	41, 263	mulcld 10060	. . . . . . . . . . . . 13
287	286	adantr 481	. . . . . . . . . . . 12 $/\$ $\$
288		elsn2g 4210	. . . . . . . . . . . 12
289	287, 288	syl 17	. . . . . . . . . . 11 $/\$ $\$
290	285, 289	mtbird 315	. . . . . . . . . 10 $/\$ $\$
291	223, 290	eldifd 3585	. . . . . . . . 9 $/\$ $\$ $\$
292	224, 291	eqeltrd 2701	. . . . . . . 8 $/\$ $\$ $\$ $\$
293		sinf 14854	. . . . . . . . . . . 12
294	293	fdmi 6052	. . . . . . . . . . 11
295	294	eqcomi 2631	. . . . . . . . . 10
296	295	a1i 11	. . . . . . . . 9 $/\$ $\$
297	296	difeq1d 3727	. . . . . . . 8 $/\$ $\$ $\$ $\$
298	292, 297	eleqtrd 2703	. . . . . . 7 $/\$ $\$ $\$ $\$
299	298	ralrimiva 2966	. . . . . 6 $\$ $\$ $\$
300		fnfvrnss 6390	. . . . . 6 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
301	210, 299, 300	syl2anc 693	. . . . 5 $\$ $\$
302		uncom 3757	. . . . . . . . . 10 $\$ $\$
303	302	a1i 11	. . . . . . . . 9 $\$ $\$
304	27	snssd 4340	. . . . . . . . . 10
305		undif 4049	. . . . . . . . . 10 $\$
306	304, 305	sylib 208	. . . . . . . . 9 $\$
307	303, 306	eqtrd 2656	. . . . . . . 8 $\$
308	307	mpteq1d 4738	. . . . . . 7 $\$ $\$ $\$
309		iftrue 4092	. . . . . . . . . . . . 13 $\$
310		oveq2 6658	. . . . . . . . . . . . 13
311	309, 310	eqtr4d 2659	. . . . . . . . . . . 12 $\$
312	311	adantl 482	. . . . . . . . . . 11 $/\$ $/\$ $\$
313		iffalse 4095	. . . . . . . . . . . . 13 $\$ $\$
314	313	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
315		eqidd 2623	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
316		oveq2 6658	. . . . . . . . . . . . . 14
317	316	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
318		simpl 473	. . . . . . . . . . . . . . 15 $/\$
319		id 22	. . . . . . . . . . . . . . . . 17
320		velsn 4193	. . . . . . . . . . . . . . . . 17
321	319, 320	sylnibr 319	. . . . . . . . . . . . . . . 16
322	321	adantl 482	. . . . . . . . . . . . . . 15 $/\$
323	318, 322	eldifd 3585	. . . . . . . . . . . . . 14 $/\$ $\$
324	323	adantll 750	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
325	41	adantr 481	. . . . . . . . . . . . . . 15 $/\$
326		elioore 12205	. . . . . . . . . . . . . . . . 17
327	326	recnd 10068	. . . . . . . . . . . . . . . 16
328	327	adantl 482	. . . . . . . . . . . . . . 15 $/\$
329	325, 328	mulcld 10060	. . . . . . . . . . . . . 14 $/\$
330	329	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$
331	315, 317, 324, 330	fvmptd 6288	. . . . . . . . . . . 12 $/\$ $/\$ $\$
332	314, 331	eqtrd 2656	. . . . . . . . . . 11 $/\$ $/\$ $\$
333	312, 332	pm2.61dan 832	. . . . . . . . . 10 $/\$ $\$
334	333	mpteq2dva 4744	. . . . . . . . 9 $\$
335		ioosscn 39716	. . . . . . . . . . . . . 14
336		resmpt 5449	. . . . . . . . . . . . . 14
337	335, 336	ax-mp 5	. . . . . . . . . . . . 13
338		eqid 2622	. . . . . . . . . . . . . . . . 17
339	338	mulc1cncf 22708	. . . . . . . . . . . . . . . 16
340	41, 339	syl 17	. . . . . . . . . . . . . . 15
341	51	cnfldtop 22587	. . . . . . . . . . . . . . . . . . 19 ℂ_fld
342		unicntop 22589	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld
343	342	restid 16094	. . . . . . . . . . . . . . . . . . 19 ℂ_fld ℂ_fld ↾_t ℂ_fld
344	341, 343	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ℂ_fld ↾_t ℂ_fld
345	344	eqcomi 2631	. . . . . . . . . . . . . . . . 17 ℂ_fld ℂ_fld ↾_t
346	51, 345, 345	cncfcn 22712	. . . . . . . . . . . . . . . 16 $/\$ ℂ_fld ℂ_fld
347	74, 75, 346	sylancr 695	. . . . . . . . . . . . . . 15 ℂ_fld ℂ_fld
348	340, 347	eleqtrd 2703	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld
349	2, 37	syl5ss 3614	. . . . . . . . . . . . . 14
350	342	cnrest 21089	. . . . . . . . . . . . . 14 ℂ_fld ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
351	348, 349, 350	syl2anc 693	. . . . . . . . . . . . 13 ℂ_fld ↾_t ℂ_fld
352	337, 351	syl5eqelr 2706	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
353	51	cnfldtopon 22586	. . . . . . . . . . . . . 14 ℂ_fld TopOn
354		resttopon 20965	. . . . . . . . . . . . . 14 ℂ_fld TopOn $/\$ ℂ_fld ↾_t TopOn
355	353, 349, 354	sylancr 695	. . . . . . . . . . . . 13 ℂ_fld ↾_t TopOn
356		cncnp 21084	. . . . . . . . . . . . 13 ℂ_fld ↾_t TopOn $/\$ ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
357	355, 353, 356	sylancl 694	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
358	352, 357	mpbid 222	. . . . . . . . . . 11 $/\$ ℂ_fld ↾_t ℂ_fld
359	358	simprd 479	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld
360		fveq2 6191	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld ℂ_fld ↾_t ℂ_fld
361	360	eleq2d 2687	. . . . . . . . . . 11 ℂ_fld ↾_t ℂ_fld ℂ_fld ↾_t ℂ_fld
362	361	rspccva 3308	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
363	359, 27, 362	syl2anc 693	. . . . . . . . 9 ℂ_fld ↾_t ℂ_fld
364	334, 363	eqeltrd 2701	. . . . . . . 8 $\$ ℂ_fld ↾_t ℂ_fld
365	307	eqcomd 2628	. . . . . . . . . . 11 $\$
366	365	oveq2d 6666	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld ↾_t $\$
367	366	oveq1d 6665	. . . . . . . . 9 ℂ_fld ↾_t ℂ_fld ℂ_fld ↾_t $\$ ℂ_fld
368	367	fveq1d 6193	. . . . . . . 8 ℂ_fld ↾_t ℂ_fld ℂ_fld ↾_t $\$ ℂ_fld
369	364, 368	eleqtrd 2703	. . . . . . 7 $\$ ℂ_fld ↾_t $\$ ℂ_fld
370	308, 369	eqeltrd 2701	. . . . . 6 $\$ $\$ ℂ_fld ↾_t $\$ ℂ_fld
371		eqid 2622	. . . . . . 7 ℂ_fld ↾_t $\$ ℂ_fld ↾_t $\$
372		eqid 2622	. . . . . . 7 $\$ $\$ $\$ $\$
373	206, 208	fmptd 6385	. . . . . . 7 $\$ $\$
374	4, 36	syl6ss 3615	. . . . . . 7 $\$
375	371, 51, 372, 373, 374, 263	ellimc 23637	. . . . . 6 $\$ lim $\$ $\$ ℂ_fld ↾_t $\$ ℂ_fld
376	370, 375	mpbird 247	. . . . 5 $\$ lim
377	134	a1i 11	. . . . . . . . . . . 12
378	238	a1i 11	. . . . . . . . . . . 12
379	154, 155, 377, 378	mulne0d 10679	. . . . . . . . . . 11
380	263, 156, 379	divcan1d 10802	. . . . . . . . . 10
381	380	eqcomd 2628	. . . . . . . . 9
382	381	oveq2d 6666	. . . . . . . 8
383	382	fveq2d 6195	. . . . . . 7
384	263, 156, 379	divcld 10801	. . . . . . . . . . 11
385	41, 384, 156	mul12d 10245	. . . . . . . . . 10
386	41, 154, 155	mulassd 10063	. . . . . . . . . . . 12
387	386	eqcomd 2628	. . . . . . . . . . 11
388	387	oveq2d 6666	. . . . . . . . . 10
389	38, 40, 154	adddird 10065	. . . . . . . . . . . . 13
390	154, 377	recid2d 10797	. . . . . . . . . . . . . 14
391	390	oveq2d 6666	. . . . . . . . . . . . 13
392	389, 391	eqtrd 2656	. . . . . . . . . . . 12
393	392	oveq1d 6665	. . . . . . . . . . 11
394	393	oveq2d 6666	. . . . . . . . . 10
395	385, 388, 394	3eqtrd 2660	. . . . . . . . 9
396	38, 154	mulcld 10060	. . . . . . . . . . 11
397		1cnd 10056	. . . . . . . . . . 11
398	396, 397	addcld 10059	. . . . . . . . . 10
399	384, 398, 155	mulassd 10063	. . . . . . . . 9
400	395, 399	eqtr4d 2659	. . . . . . . 8
401	400	fveq2d 6195	. . . . . . 7
402		mod0 12675	. . . . . . . . . . 11 $/\$
403	57, 253, 402	sylancl 694	. . . . . . . . . 10
404	282, 403	mpbid 222	. . . . . . . . 9
405	5	nnzd 11481	. . . . . . . . . . 11
406		2z 11409	. . . . . . . . . . . 12
407	406	a1i 11	. . . . . . . . . . 11
408	405, 407	zmulcld 11488	. . . . . . . . . 10
409	408	peano2zd 11485	. . . . . . . . 9
410	404, 409	zmulcld 11488	. . . . . . . 8
411		sinkpi 24271	. . . . . . . 8
412	410, 411	syl 17	. . . . . . 7
413	383, 401, 412	3eqtrd 2660	. . . . . 6
414		sincn 24198	. . . . . . . 8
415	414	a1i 11	. . . . . . 7
416	415, 286	cnlimci 23653	. . . . . 6 lim
417	413, 416	eqeltrrd 2702	. . . . 5 lim
418	301, 376, 417	limccog 39852	. . . 4 $\$ lim
419	14	a1i 11	. . . . . . . . 9 $/\$ $\$ $\$
420	213	fveq2d 6195	. . . . . . . . 9 $/\$ $\$ $/\$
421	223	sincld 14860	. . . . . . . . 9 $/\$ $\$
422	419, 420, 214, 421	fvmptd 6288	. . . . . . . 8 $/\$ $\$
423	224	fveq2d 6195	. . . . . . . 8 $/\$ $\$ $\$
424	422, 423	eqtr4d 2659	. . . . . . 7 $/\$ $\$ $\$
425	424	mpteq2dva 4744	. . . . . 6 $\$ $\$ $\$
426	15	feqmptd 6249	. . . . . 6 $\$
427		fcompt 6400	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$ $\$
428	293, 373, 427	sylancr 695	. . . . . 6 $\$ $\$ $\$
429	425, 426, 428	3eqtr4rd 2667	. . . . 5 $\$
430	429	oveq1d 6665	. . . 4 $\$ lim lim
431	418, 430	eleqtrd 2703	. . 3 lim
432		simpr 477	. . . . . . . . . 10 $/\$ $/\$
433	432	iftrued 4094	. . . . . . . . 9 $/\$ $/\$
434	263, 154, 156, 377, 379	divdiv32d 10826	. . . . . . . . . . . . . . . . 17
435	434	oveq1d 6665	. . . . . . . . . . . . . . . 16
436	263	halfcld 11277	. . . . . . . . . . . . . . . . 17
437	436, 156, 379	divcan1d 10802	. . . . . . . . . . . . . . . 16
438	384, 154, 156, 377	div32d 10824	. . . . . . . . . . . . . . . . 17
439	155, 154, 377	divcan3d 10806	. . . . . . . . . . . . . . . . . 18
440	439	oveq2d 6666	. . . . . . . . . . . . . . . . 17
441	438, 440	eqtrd 2656	. . . . . . . . . . . . . . . 16
442	435, 437, 441	3eqtr3d 2664	. . . . . . . . . . . . . . 15
443	442	fveq2d 6195	. . . . . . . . . . . . . 14
444		sinkpi 24271	. . . . . . . . . . . . . . 15
445	404, 444	syl 17	. . . . . . . . . . . . . 14
446	443, 445	eqtrd 2656	. . . . . . . . . . . . 13
447	446	oveq2d 6666	. . . . . . . . . . . 12
448	156	mul01d 10235	. . . . . . . . . . . 12
449	447, 448	eqtrd 2656	. . . . . . . . . . 11
450	449	eqcomd 2628	. . . . . . . . . 10
451	450	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$
452		oveq1 6657	. . . . . . . . . . . . 13
453	452	fveq2d 6195	. . . . . . . . . . . 12
454	453	oveq2d 6666	. . . . . . . . . . 11
455	454	eqcomd 2628	. . . . . . . . . 10
456	455	adantl 482	. . . . . . . . 9 $/\$ $/\$
457	433, 451, 456	3eqtrd 2660	. . . . . . . 8 $/\$ $/\$
458		iffalse 4095	. . . . . . . . . 10
459	458	adantl 482	. . . . . . . . 9 $/\$ $/\$
460	23	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $\$
461		oveq1 6657	. . . . . . . . . . . . 13
462	461	fveq2d 6195	. . . . . . . . . . . 12
463	462	oveq2d 6666	. . . . . . . . . . 11
464	463	adantl 482	. . . . . . . . . 10 $/\$ $/\$ $/\$
465	120	a1i 11	. . . . . . . . . . . 12 $/\$
466	328	halfcld 11277	. . . . . . . . . . . . 13 $/\$
467	466	sincld 14860	. . . . . . . . . . . 12 $/\$
468	465, 467	mulcld 10060	. . . . . . . . . . 11 $/\$
469	468	adantr 481	. . . . . . . . . 10 $/\$ $/\$
470	460, 464, 324, 469	fvmptd 6288	. . . . . . . . 9 $/\$ $/\$
471	459, 470	eqtrd 2656	. . . . . . . 8 $/\$ $/\$
472	457, 471	pm2.61dan 832	. . . . . . 7 $/\$
473	472	mpteq2dva 4744	. . . . . 6
474		eqid 2622	. . . . . . . . . . 11
475	75, 156, 75	constcncfg 40084	. . . . . . . . . . . 12
476		id 22	. . . . . . . . . . . . . . . . 17
477		2cnd 11093	. . . . . . . . . . . . . . . . 17
478	134	a1i 11	. . . . . . . . . . . . . . . . 17
479	476, 477, 478	divrec2d 10805	. . . . . . . . . . . . . . . 16
480	479	mpteq2ia 4740	. . . . . . . . . . . . . . 15
481		eqid 2622	. . . . . . . . . . . . . . . . 17
482	481	mulc1cncf 22708	. . . . . . . . . . . . . . . 16
483	39, 482	ax-mp 5	. . . . . . . . . . . . . . 15
484	480, 483	eqeltri 2697	. . . . . . . . . . . . . 14
485	484	a1i 11	. . . . . . . . . . . . 13
486	415, 485	cncfmpt1f 22716	. . . . . . . . . . . 12
487	475, 486	mulcncf 23215	. . . . . . . . . . 11
488	474, 487, 349, 75, 468	cncfmptssg 40083	. . . . . . . . . 10
489		eqid 2622	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld ↾_t
490	51, 489, 345	cncfcn 22712	. . . . . . . . . . 11 $/\$ ℂ_fld ↾_t ℂ_fld
491	349, 74, 490	sylancl 694	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld
492	488, 491	eleqtrd 2703	. . . . . . . . 9 ℂ_fld ↾_t ℂ_fld
493		cncnp 21084	. . . . . . . . . 10 ℂ_fld ↾_t TopOn $/\$ ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
494	355, 353, 493	sylancl 694	. . . . . . . . 9 ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
495	492, 494	mpbid 222	. . . . . . . 8 $/\$ ℂ_fld ↾_t ℂ_fld
496	495	simprd 479	. . . . . . 7 ℂ_fld ↾_t ℂ_fld
497	360	eleq2d 2687	. . . . . . . 8 ℂ_fld ↾_t ℂ_fld ℂ_fld ↾_t ℂ_fld
498	497	rspccva 3308	. . . . . . 7 ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
499	496, 27, 498	syl2anc 693	. . . . . 6 ℂ_fld ↾_t ℂ_fld
500	473, 499	eqeltrd 2701	. . . . 5 ℂ_fld ↾_t ℂ_fld
501	307	mpteq1d 4738	. . . . 5 $\$
502	366	eqcomd 2628	. . . . . . 7 ℂ_fld ↾_t $\$ ℂ_fld ↾_t
503	502	oveq1d 6665	. . . . . 6 ℂ_fld ↾_t $\$ ℂ_fld ℂ_fld ↾_t ℂ_fld
504	503	fveq1d 6193	. . . . 5 ℂ_fld ↾_t $\$ ℂ_fld ℂ_fld ↾_t ℂ_fld
505	500, 501, 504	3eltr4d 2716	. . . 4 $\$ ℂ_fld ↾_t $\$ ℂ_fld
506		eqid 2622	. . . . 5 $\$ $\$
507	11, 124	syldan 487	. . . . . 6 $/\$ $\$
508	507, 23	fmptd 6385	. . . . 5 $\$
509	371, 51, 506, 508, 374, 263	ellimc 23637	. . . 4 lim $\$ ℂ_fld ↾_t $\$ ℂ_fld
510	505, 509	mpbird 247	. . 3 lim
511	256	nrexdv 3001	. . . 4 $\$
512		ffun 6048	. . . . . . 7 $\$
513	508, 512	syl 17	. . . . . 6
514		fvelima 6248	. . . . . 6 $/\$ $\$ $\$
515	513, 514	sylan 488	. . . . 5 $/\$ $\$ $\$
516		2cnd 11093	. . . . . . . . . . . . 13 $/\$ $\$
517	119	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
518	134	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
519	238	a1i 11	. . . . . . . . . . . . 13 $/\$ $\$
520	105, 516, 517, 518, 519	divdiv1d 10832	. . . . . . . . . . . 12 $/\$ $\$
521	520	eqcomd 2628	. . . . . . . . . . 11 $/\$ $\$
522	521	adantr 481	. . . . . . . . . 10 $/\$ $\$ $/\$
523		2cnd 11093	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
524	119	a1i 11	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
525	523, 524	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
526	232	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
527	526	halfcld 11277	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
528	527	sincld 14860	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
529	525, 528	mulcld 10060	. . . . . . . . . . . . . . . . 17 $\$ $/\$
530	23	fvmpt2 6291	. . . . . . . . . . . . . . . . 17 $\$ $/\$
531	529, 530	syldan 487	. . . . . . . . . . . . . . . 16 $\$ $/\$
532	531	eqcomd 2628	. . . . . . . . . . . . . . 15 $\$ $/\$
533		simpr 477	. . . . . . . . . . . . . . 15 $\$ $/\$
534	532, 533	eqtrd 2656	. . . . . . . . . . . . . 14 $\$ $/\$
535	120	a1i 11	. . . . . . . . . . . . . . . 16 $\$
536	232	halfcld 11277	. . . . . . . . . . . . . . . . 17 $\$
537	536	sincld 14860	. . . . . . . . . . . . . . . 16 $\$
538	535, 537	mul0ord 10677	. . . . . . . . . . . . . . 15 $\$ $\/$
539	538	adantr 481	. . . . . . . . . . . . . 14 $\$ $/\$ $\/$
540	534, 539	mpbid 222	. . . . . . . . . . . . 13 $\$ $/\$ $\/$
541		2cnne0 11242	. . . . . . . . . . . . . . 15 $/\$
542	119, 238	pm3.2i 471	. . . . . . . . . . . . . . 15 $/\$
543		mulne0 10669	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
544	541, 542, 543	mp2an 708	. . . . . . . . . . . . . 14
545	544	neii 2796	. . . . . . . . . . . . 13
546		pm2.53 388	. . . . . . . . . . . . 13 $\/$
547	540, 545, 546	mpisyl 21	. . . . . . . . . . . 12 $\$ $/\$
548	547	adantll 750	. . . . . . . . . . 11 $/\$ $\$ $/\$
549	105	adantr 481	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
550	549	halfcld 11277	. . . . . . . . . . . 12 $/\$ $\$ $/\$
551	550, 246	syl 17	. . . . . . . . . . 11 $/\$ $\$ $/\$
552	548, 551	mpbid 222	. . . . . . . . . 10 $/\$ $\$ $/\$
553	522, 552	eqeltrd 2701	. . . . . . . . 9 $/\$ $\$ $/\$
554	11	adantr 481	. . . . . . . . . 10 $/\$ $\$ $/\$
555	554, 253, 254	sylancl 694	. . . . . . . . 9 $/\$ $\$ $/\$
556	553, 555	mpbird 247	. . . . . . . 8 $/\$ $\$ $/\$
557	556	ex 450	. . . . . . 7 $/\$ $\$
558	557	reximdva 3017	. . . . . 6 $\$ $\$
559	558	adantr 481	. . . . 5 $/\$ $\$ $\$ $\$
560	515, 559	mpd 15	. . . 4 $/\$ $\$ $\$
561	511, 560	mtand 691	. . 3 $\$
562		simpr 477	. . . . . . . . 9 $/\$ $\$ $\$
563	111	fvmpt2 6291	. . . . . . . . 9 $\$ $/\$
564	562, 201, 563	syl2anc 693	. . . . . . . 8 $/\$ $\$
565	536	coscld 14861	. . . . . . . . . 10 $\$
566	565	adantl 482	. . . . . . . . 9 $/\$ $\$
567		dirkercncflem2.11	. . . . . . . . 9 $/\$ $\$
568	517, 566, 519, 567	mulne0d 10679	. . . . . . . 8 $/\$ $\$
569	564, 568	eqnetrd 2861	. . . . . . 7 $/\$ $\$
570	569	neneqd 2799	. . . . . 6 $/\$ $\$
571	570	nrexdv 3001	. . . . 5 $\$
572	201, 111	fmptd 6385	. . . . . . 7 $\$
573		ffun 6048	. . . . . . 7 $\$
574	572, 573	syl 17	. . . . . 6
575		fvelima 6248	. . . . . 6 $/\$ $\$ $\$
576	574, 575	sylan 488	. . . . 5 $/\$ $\$ $\$
577	571, 576	mtand 691	. . . 4 $\$
578	199	imaeq1d 5465	. . . 4 $\$ $\$
579	577, 578	neleqtrrd 2723	. . 3 $\$
580		dirkercncflem2.d	. . . . . 6
581	580	dirkerval2 40311	. . . . 5 $/\$
582	5, 57, 581	syl2anc 693	. . . 4
583	282	iftrued 4094	. . . . 5
584		dirkercncflem2.l	. . . . . . . . . . 11
585	584	a1i 11	. . . . . . . . . 10
586		iftrue 4092	. . . . . . . . . . . . . 14 $\$
587	586	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
588	154, 38	mulcld 10060	. . . . . . . . . . . . . . . . . 18
589	588, 397	addcld 10059	. . . . . . . . . . . . . . . . 17
590	589, 154, 155, 377, 378	divdiv1d 10832	. . . . . . . . . . . . . . . 16
591	590	eqcomd 2628	. . . . . . . . . . . . . . 15
592	588, 397, 154, 377	divdird 10839	. . . . . . . . . . . . . . . . 17
593	38, 154, 377	divcan3d 10806	. . . . . . . . . . . . . . . . . 18
594	593	oveq1d 6665	. . . . . . . . . . . . . . . . 17
595	592, 594	eqtrd 2656	. . . . . . . . . . . . . . . 16
596	595	oveq1d 6665	. . . . . . . . . . . . . . 15
597	591, 596	eqtrd 2656	. . . . . . . . . . . . . 14
598	597	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$
599	310	fveq2d 6195	. . . . . . . . . . . . . . . . 17
600	599	oveq2d 6666	. . . . . . . . . . . . . . . 16
601	452	fveq2d 6195	. . . . . . . . . . . . . . . . 17
602	601	oveq2d 6666	. . . . . . . . . . . . . . . 16
603	600, 602	oveq12d 6668	. . . . . . . . . . . . . . 15
604	603	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
605	38, 40, 263	adddird 10065	. . . . . . . . . . . . . . . . . . . . 21
606	397, 154, 263, 377	div32d 10824	. . . . . . . . . . . . . . . . . . . . . . 23
607	436	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . 23
608	606, 607	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22
609	608	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21
610	38, 263	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . 22
611	610, 436	addcomd 10238	. . . . . . . . . . . . . . . . . . . . 21
612	605, 609, 611	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20
613	612	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
614	610, 156, 379	divcan1d 10802	. . . . . . . . . . . . . . . . . . . . . 22
615	614	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21
616	615	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
617	616	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
618	38, 263, 156, 379	divassd 10836	. . . . . . . . . . . . . . . . . . . . 21
619	405, 404	zmulcld 11488	. . . . . . . . . . . . . . . . . . . . 21
620	618, 619	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20
621		cosper 24234	. . . . . . . . . . . . . . . . . . . 20 $/\$
622	436, 620, 621	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
623	613, 617, 622	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18
624	623	oveq2d 6666	. . . . . . . . . . . . . . . . 17
625	624	oveq1d 6665	. . . . . . . . . . . . . . . 16
626	436	coscld 14861	. . . . . . . . . . . . . . . . 17
627	263, 154, 155, 377, 378	divdiv1d 10832	. . . . . . . . . . . . . . . . . . . . 21
628	627, 404	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20
629	628	zred 11482	. . . . . . . . . . . . . . . . . . . . 21
630	629, 272	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . 20
631		halflt1 11250	. . . . . . . . . . . . . . . . . . . . . 22
632	631	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
633	268, 267, 629, 632	ltadd2dd 10196	. . . . . . . . . . . . . . . . . . . 20
634		btwnnz 11453	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
635	628, 630, 633, 634	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19
636		coseq0 40075	. . . . . . . . . . . . . . . . . . . 20
637	436, 636	syl 17	. . . . . . . . . . . . . . . . . . 19
638	635, 637	mtbird 315	. . . . . . . . . . . . . . . . . 18
639	638	neqned 2801	. . . . . . . . . . . . . . . . 17
640	41, 155, 626, 378, 639	divcan5rd 10828	. . . . . . . . . . . . . . . 16
641	625, 640	eqtrd 2656	. . . . . . . . . . . . . . 15
642	641	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
643	604, 642	eqtr2d 2657	. . . . . . . . . . . . 13 $/\$ $/\$
644	587, 598, 643	3eqtrrd 2661	. . . . . . . . . . . 12 $/\$ $/\$ $\$
645		iffalse 4095	. . . . . . . . . . . . . 14 $\$ $\$
646	645	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
647		eqidd 2623	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
648		fveq2 6191	. . . . . . . . . . . . . . . 16
649		fveq2 6191	. . . . . . . . . . . . . . . 16
650	648, 649	oveq12d 6668	. . . . . . . . . . . . . . 15
651	650	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
652	106, 100	fmptd 6385	. . . . . . . . . . . . . . . . 17 $\$
653	652	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
654	653, 324	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ $/\$
655	572	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
656	655, 324	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ $/\$
657	111	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
658		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
659	658	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
660	659	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
661	660	oveq2d 6666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
662	119	a1i 11	. . . . . . . . . . . . . . . . . . 19
663	327	halfcld 11277	. . . . . . . . . . . . . . . . . . . 20
664	663	coscld 14861	. . . . . . . . . . . . . . . . . . 19
665	662, 664	mulcld 10060	. . . . . . . . . . . . . . . . . 18
666	665	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
667	657, 661, 324, 666	fvmptd 6288	. . . . . . . . . . . . . . . 16 $/\$ $/\$
668	542	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
669	664	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
670		simpll 790	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
671	461	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
672	671	neeq1d 2853	. . . . . . . . . . . . . . . . . . . 20
673	226, 672	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
674	673, 567	chvarv 2263	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
675	670, 324, 674	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
676		mulne0 10669	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
677	668, 669, 675, 676	syl12anc 1324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
678	667, 677	eqnetrd 2861	. . . . . . . . . . . . . . 15 $/\$ $/\$
679	654, 656, 678	divcld 10801	. . . . . . . . . . . . . 14 $/\$ $/\$
680	647, 651, 324, 679	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
681	100	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
682	317	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
683	682	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
684	329	coscld 14861	. . . . . . . . . . . . . . . . 17 $/\$
685	325, 684	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$
686	685	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
687	681, 683, 324, 686	fvmptd 6288	. . . . . . . . . . . . . 14 $/\$ $/\$
688	687, 667	oveq12d 6668	. . . . . . . . . . . . 13 $/\$ $/\$
689	646, 680, 688	3eqtrrd 2661	. . . . . . . . . . . 12 $/\$ $/\$ $\$
690	644, 689	pm2.61dan 832	. . . . . . . . . . 11 $/\$ $\$
691	690	mpteq2dva 4744	. . . . . . . . . 10 $\$
692	585, 691	eqtr2d 2657	. . . . . . . . 9 $\$
693	349, 41, 75	constcncfg 40084	. . . . . . . . . . . . . . . 16
694		cosf 14855	. . . . . . . . . . . . . . . . . . 19
695	231, 44	sylan2 491	. . . . . . . . . . . . . . . . . . . 20 $/\$
696		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
697	695, 696	fmptd 6385	. . . . . . . . . . . . . . . . . . 19
698		fcompt 6400	. . . . . . . . . . . . . . . . . . 19 $/\$
699	694, 697, 698	sylancr 695	. . . . . . . . . . . . . . . . . 18
700		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21 $/\$
701	316	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
702		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
703	700, 701, 702, 329	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20 $/\$
704	703	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 $/\$
705	704	mpteq2dva 4744	. . . . . . . . . . . . . . . . . 18
706	699, 705	eqtr2d 2657	. . . . . . . . . . . . . . . . 17
707	349, 41, 75	constcncfg 40084	. . . . . . . . . . . . . . . . . . 19
708	349, 75	idcncfg 40085	. . . . . . . . . . . . . . . . . . 19
709	707, 708	mulcncf 23215	. . . . . . . . . . . . . . . . . 18
710		coscn 24199	. . . . . . . . . . . . . . . . . . 19
711	710	a1i 11	. . . . . . . . . . . . . . . . . 18
712	709, 711	cncfco 22710	. . . . . . . . . . . . . . . . 17
713	706, 712	eqeltrd 2701	. . . . . . . . . . . . . . . 16
714	693, 713	mulcncf 23215	. . . . . . . . . . . . . . 15
715		eqid 2622	. . . . . . . . . . . . . . . 16
716	349, 155, 75	constcncfg 40084	. . . . . . . . . . . . . . . . 17
717		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21 $/\$
718	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
719	328, 717, 718	divrecd 10804	. . . . . . . . . . . . . . . . . . . 20 $/\$
720	719	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19
721		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
722		cncfmptid 22715	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
723	74, 74, 722	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22
724	723	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
725	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
726		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
727	725, 726, 725	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . 22
728	39, 727	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21
729	724, 728	mulcncf 23215	. . . . . . . . . . . . . . . . . . . 20
730	719, 466	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20 $/\$
731	721, 729, 349, 75, 730	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . 19
732	720, 731	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18
733	711, 732	cncfmpt1f 22716	. . . . . . . . . . . . . . . . 17
734	716, 733	mulcncf 23215	. . . . . . . . . . . . . . . 16
735		ssid 3624	. . . . . . . . . . . . . . . . 17
736	735	a1i 11	. . . . . . . . . . . . . . . 16
737		difssd 3738	. . . . . . . . . . . . . . . 16 $\$
738	665	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
739	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
740	664	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
741	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
742	601	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
743	639	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
744	742, 743	eqnetrd 2861	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
745	744	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
746	745, 675	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20 $/\$
747	739, 740, 741, 746	mulne0d 10679	. . . . . . . . . . . . . . . . . . 19 $/\$
748	747	neneqd 2799	. . . . . . . . . . . . . . . . . 18 $/\$
749		elsng 4191	. . . . . . . . . . . . . . . . . . 19
750	738, 749	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
751	748, 750	mtbird 315	. . . . . . . . . . . . . . . . 17 $/\$
752	738, 751	eldifd 3585	. . . . . . . . . . . . . . . 16 $/\$ $\$
753	715, 734, 736, 737, 752	cncfmptssg 40083	. . . . . . . . . . . . . . 15 $\$
754	714, 753	divcncf 23216	. . . . . . . . . . . . . 14
755	754, 491	eleqtrd 2703	. . . . . . . . . . . . 13 ℂ_fld ↾_t ℂ_fld
756	585, 755	eqeltrd 2701	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld
757		cncnp 21084	. . . . . . . . . . . . 13 ℂ_fld ↾_t TopOn $/\$ ℂ_fld TopOn ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
758	355, 353, 757	sylancl 694	. . . . . . . . . . . 12 ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
759	756, 758	mpbid 222	. . . . . . . . . . 11 $/\$ ℂ_fld ↾_t ℂ_fld
760	759	simprd 479	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld
761	360	eleq2d 2687	. . . . . . . . . . 11 ℂ_fld ↾_t ℂ_fld ℂ_fld ↾_t ℂ_fld
762	761	rspccva 3308	. . . . . . . . . 10 ℂ_fld ↾_t ℂ_fld $/\$ ℂ_fld ↾_t ℂ_fld
763	760, 27, 762	syl2anc 693	. . . . . . . . 9 ℂ_fld ↾_t ℂ_fld
764	692, 763	eqeltrd 2701	. . . . . . . 8 $\$ ℂ_fld ↾_t ℂ_fld
765	307	mpteq1d 4738	. . . . . . . 8 $\$ $\$ $\$
766	764, 765, 504	3eltr4d 2716	. . . . . . 7 $\$ $\$ ℂ_fld ↾_t $\$ ℂ_fld
767		eqid 2622	. . . . . . . 8 $\$ $\$ $\$ $\$
768	100	fvmpt2 6291	. . . . . . . . . . . 12 $\$ $/\$
769	562, 106, 768	syl2anc 693	. . . . . . . . . . 11 $/\$ $\$
770	769, 564	oveq12d 6668	. . . . . . . . . 10 $/\$ $\$
771	106, 201, 568	divcld 10801	. . . . . . . . . 10 $/\$ $\$
772	770, 771	eqeltrd 2701	. . . . . . . . 9 $/\$ $\$
773		eqid 2622	. . . . . . . . 9 $\$ $\$
774	772, 773	fmptd 6385	. . . . . . . 8 $\$ $\$
775	371, 51, 767, 774, 374, 263	ellimc 23637	. . . . . . 7 $\$ lim $\$ $\$ ℂ_fld ↾_t $\$ ℂ_fld
776	766, 775	mpbird 247	. . . . . 6 $\$ lim
777	103	eqcomd 2628	. . . . . . . . . 10
778	777	fveq1d 6193	. . . . . . . . 9
779	199	eqcomd 2628	. . . . . . . . . 10
780	779	fveq1d 6193	. . . . . . . . 9
781	778, 780	oveq12d 6668	. . . . . . . 8
782	781	mpteq2dv 4745	. . . . . . 7 $\$ $\$
783	782	oveq1d 6665	. . . . . 6 $\$ lim $\$ lim
784	776, 783	eleqtrd 2703	. . . . 5 $\$ lim
785	583, 784	eqeltrd 2701	. . . 4 $\$ lim
786	582, 785	eqeltrd 2701	. . 3 $\$ lim
787	4, 15, 24, 26, 27, 28, 110, 205, 431, 510, 561, 579, 786	lhop 23779	. 2 $\$ lim
788	580	dirkerval 40308	. . . . . 6
789	5, 788	syl 17	. . . . 5
790	789	reseq1d 5395	. . . 4 $\$ $\$
791	4	resmptd 5452	. . . 4 $\$ $\$
792	256	iffalsed 4097	. . . . . 6 $/\$ $\$
793	13	recnd 10068	. . . . . . . 8 $/\$ $\$
794	14	fvmpt2 6291	. . . . . . . 8 $\$ $/\$
795	562, 793, 794	syl2anc 693	. . . . . . 7 $/\$ $\$
796	562, 507, 530	syl2anc 693	. . . . . . 7 $/\$ $\$
797	795, 796	oveq12d 6668	. . . . . 6 $/\$ $\$
798	792, 797	eqtr4d 2659	. . . . 5 $/\$ $\$
799	798	mpteq2dva 4744	. . . 4 $\$ $\$
800	790, 791, 799	3eqtrrd 2661	. . 3 $\$ $\$
801	800	oveq1d 6665	. 2 $\$ lim $\$ lim
802	787, 801	eleqtrd 2703	1 $\$ lim

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913 $\$ cdif 3571

cun 3572

wss 3574

cif 4086

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

cres 5116

cima 5117

ccom 5118

wfun 5882

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cdiv 10684

cn 11020

c2 11070

cz 11377

crp 11832

cioo 12175

cmo 12668

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

cha 21112

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: dirkercncflem3 40322

W3C validator