cxpcn3lem - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cxpcn3lem		Unicode version

Theorem cxpcn3lem 20584

Description: Lemma for cxpcn3 20585. (Contributed by Mario Carneiro, 2-May-2016.)

**Hypotheses**
Ref	Expression
cxpcn3.d
cxpcn3.j	ℂ_fld
cxpcn3.k	↾_t
cxpcn3.l	↾_t
cxpcn3.u
cxpcn3.t

**Assertion**
Ref	Expression
cxpcn3lem	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

**Proof of Theorem cxpcn3lem**
Step	Hyp	Ref	Expression
1		cxpcn3.t	. . 3
2		cxpcn3.u	. . . . 5
3		cxpcn3.d	. . . . . . . . . . 11
4	3	eleq2i 2468	. . . . . . . . . 10
5		ref 11872	. . . . . . . . . . 11
6		ffn 5550	. . . . . . . . . . 11
7		elpreima 5809	. . . . . . . . . . 11 $/\$
8	5, 6, 7	mp2b 10	. . . . . . . . . 10 $/\$
9	4, 8	bitri 241	. . . . . . . . 9 $/\$
10	9	simprbi 451	. . . . . . . 8
11	10	adantr 452	. . . . . . 7 $/\$
12		1rp 10572	. . . . . . 7
13		ifcl 3735	. . . . . . 7 $/\$
14	11, 12, 13	sylancl 644	. . . . . 6 $/\$
15	14	rphalfcld 10616	. . . . 5 $/\$
16	2, 15	syl5eqel 2488	. . . 4 $/\$
17		simpr 448	. . . . 5 $/\$
18	16	rpreccld 10614	. . . . . 6 $/\$
19	18	rpred 10604	. . . . 5 $/\$
20	17, 19	rpcxpcld 20574	. . . 4 $/\$
21		ifcl 3735	. . . 4 $/\$
22	16, 20, 21	syl2anc 643	. . 3 $/\$
23	1, 22	syl5eqel 2488	. 2 $/\$
24		elrege0 10963	. . . 4 $/\$
25		0re 9047	. . . . . . . 8
26	25	a1i 11	. . . . . . 7 $/\$
27		leloe 9117	. . . . . . 7 $/\$ $\/$
28	26, 27	sylan 458	. . . . . 6 $/\$ $/\$ $\/$
29		elrp 10570	. . . . . . . . 9 $/\$
30		simp2l 983	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
31		simp2r 984	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
32		cnvimass 5183	. . . . . . . . . . . . . . . . . 18
33	5	fdmi 5555	. . . . . . . . . . . . . . . . . 18
34	32, 33	sseqtri 3340	. . . . . . . . . . . . . . . . 17
35	3, 34	eqsstri 3338	. . . . . . . . . . . . . . . 16
36	35	sseli 3304	. . . . . . . . . . . . . . 15
37	31, 36	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
38		abscxp 20536	. . . . . . . . . . . . . 14 $/\$
39	30, 37, 38	syl2anc 643	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
40	37	recld 11954	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
41	30, 40	rpcxpcld 20574	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
42	41	rpred 10604	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43	16	3ad2ant1 978	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
44	43	rpred 10604	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
45	30, 44	rpcxpcld 20574	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
46	45	rpred 10604	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
47		simp1r 982	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	47	rpred 10604	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49		simp1l 981	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
50	9	simplbi 447	. . . . . . . . . . . . . . . . . . 19
51	49, 50	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
52	51	recld 11954	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	rehalfcld 10170	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
54		1re 9046	. . . . . . . . . . . . . . . . . . 19
55		min1 10732	. . . . . . . . . . . . . . . . . . 19 $/\$
56	52, 54, 55	sylancl 644	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
57	14	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
58	57	rpred 10604	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
59		2re 10025	. . . . . . . . . . . . . . . . . . . 20
60	59	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
61		2pos 10038	. . . . . . . . . . . . . . . . . . . 20
62	61	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
63		lediv1 9831	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
64	58, 52, 60, 62, 63	syl112anc 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
65	56, 64	mpbid 202	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
66	2, 65	syl5eqbr 4205	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
67	52	recnd 9070	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
68	67	2halvesd 10169	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
69	51, 37	resubd 11976	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
70	51, 37	subcld 9367	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
71	70	recld 11954	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
72	70	abscld 12193	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
73	70	releabsd 12208	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
74		simp3r 986	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
75	74, 1	syl6breq 4211	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
76	20	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	rpred 10604	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
78		ltmin 10737	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
79	72, 44, 77, 78	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	75, 79	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	80	simpld 446	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
82	71, 72, 44, 73, 81	lelttrd 9184	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
83	71, 44, 53, 82, 66	ltletrd 9186	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
84	69, 83	eqbrtrrd 4194	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
85	52, 40, 53	ltsubadd2d 9580	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
86	84, 85	mpbid 202	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
87	68, 86	eqbrtrd 4192	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
88	53, 40, 53	ltadd1d 9575	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
89	87, 88	mpbird 224	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
90	44, 53, 40, 66, 89	lelttrd 9184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
91	30	rpred 10604	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
92	54	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
93	30	rprege0d 10611	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		absid 12056	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	93, 94	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
96		simp3l 985	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	eqbrtrrd 4194	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
98	97, 1	syl6breq 4211	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
99		ltmin 10737	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
100	91, 44, 77, 99	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	98, 100	mpbid 202	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	simpld 446	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
103		rehalfcl 10150	. . . . . . . . . . . . . . . . . . 19
104	54, 103	mp1i 12	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
105		min2 10733	. . . . . . . . . . . . . . . . . . . . 21 $/\$
106	52, 54, 105	sylancl 644	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
107		lediv1 9831	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
108	58, 92, 60, 62, 107	syl112anc 1188	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
109	106, 108	mpbid 202	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
110	2, 109	syl5eqbr 4205	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111		halflt1 10145	. . . . . . . . . . . . . . . . . . 19
112	111	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
113	44, 104, 92, 110, 112	lelttrd 9184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
114	91, 44, 92, 102, 113	lttrd 9187	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
115	30, 44, 114, 40	cxplt3d 20576	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	90, 115	mpbid 202	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
117	43	rpcnne0d 10613	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		recid 9648	. . . . . . . . . . . . . . . . . . 19 $/\$
119	117, 118	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
120	119	oveq2d 6056	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
121	43	rpreccld 10614	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
122	121	rpcnd 10606	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
123	30, 44, 122	cxpmuld 20578	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
124	30	rpcnd 10606	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
125	124	cxp1d 20550	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
126	120, 123, 125	3eqtr3d 2444	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
127	101	simprd 450	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
128	126, 127	eqbrtrd 4192	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
129	45	rprege0d 10611	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	47	rprege0d 10611	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131		cxplt2 20542	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
132	129, 130, 121, 131	syl3anc 1184	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
133	128, 132	mpbird 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
134	42, 46, 48, 116, 133	lttrd 9187	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
135	39, 134	eqbrtrd 4192	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
136	135	3expia 1155	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
137	136	anassrs 630	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
138	137	ralrimiva 2749	. . . . . . . . 9 $/\$ $/\$ $/\$
139	29, 138	sylan2br 463	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
140	139	expr 599	. . . . . . 7 $/\$ $/\$ $/\$
141		elpreima 5809	. . . . . . . . . . . . . . . . . . 19 $/\$
142	5, 6, 141	mp2b 10	. . . . . . . . . . . . . . . . . 18 $/\$
143	142	simprbi 451	. . . . . . . . . . . . . . . . 17
144	143, 3	eleq2s 2496	. . . . . . . . . . . . . . . 16
145	144	rpne0d 10609	. . . . . . . . . . . . . . 15
146		fveq2 5687	. . . . . . . . . . . . . . . . 17
147		re0 11912	. . . . . . . . . . . . . . . . 17
148	146, 147	syl6eq 2452	. . . . . . . . . . . . . . . 16
149	148	necon3i 2606	. . . . . . . . . . . . . . 15
150	145, 149	syl 16	. . . . . . . . . . . . . 14
151	36, 150	0cxpd 20554	. . . . . . . . . . . . 13
152	151	adantl 453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	152	abs00bd 12051	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154		simpllr 736	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
155	154	rpgt0d 10607	. . . . . . . . . . 11 $/\$ $/\$ $/\$
156	153, 155	eqbrtrd 4192	. . . . . . . . . 10 $/\$ $/\$ $/\$
157		oveq1 6047	. . . . . . . . . . . 12
158	157	fveq2d 5691	. . . . . . . . . . 11
159	158	breq1d 4182	. . . . . . . . . 10
160	156, 159	syl5ibcom 212	. . . . . . . . 9 $/\$ $/\$ $/\$
161	160	a1dd 44	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
162	161	ralrimdva 2756	. . . . . . 7 $/\$ $/\$ $/\$
163	140, 162	jaod 370	. . . . . 6 $/\$ $/\$ $\/$ $/\$
164	28, 163	sylbid 207	. . . . 5 $/\$ $/\$ $/\$
165	164	expimpd 587	. . . 4 $/\$ $/\$ $/\$
166	24, 165	syl5bi 209	. . 3 $/\$ $/\$
167	166	ralrimiv 2748	. 2 $/\$ $/\$
168		breq2 4176	. . . . . 6
169		breq2 4176	. . . . . 6
170	168, 169	anbi12d 692	. . . . 5 $/\$ $/\$
171	170	imbi1d 309	. . . 4 $/\$ $/\$
172	171	2ralbidv 2708	. . 3 $/\$ $/\$
173	172	rspcev 3012	. 2 $/\$ $/\$ $/\$
174	23, 167, 173	syl2anc 643	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cif 3699 class class class wbr 4172

ccnv 4836

cdm 4837

cima 4840

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

cpnf 9073

clt 9076

cle 9077

cmin 9247

cdiv 9633

c2 10005

crp 10568

cico 10874

cre 11857

cabs 11994 ↾_t crest 13603

ctopn 13604 ℂ_fldccnfld 16658

ccxp 20406

This theorem is referenced by: cxpcn3 20585

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407 df-cxp 20408

W3C validator