cxpcn3lem - Metamath Proof Explorer

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

Theorem cxpcn3lem 23685

Description: Lemma for cxpcn3 23686. (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 2499	. . . . . . . . . 10
5		ref 13175	. . . . . . . . . . 11
6		ffn 5746	. . . . . . . . . . 11
7		elpreima 6017	. . . . . . . . . . 11 $/\$
8	5, 6, 7	mp2b 10	. . . . . . . . . 10 $/\$
9	4, 8	bitri 252	. . . . . . . . 9 $/\$
10	9	simprbi 465	. . . . . . . 8
11	10	adantr 466	. . . . . . 7 $/\$
12		1rp 11313	. . . . . . 7
13		ifcl 3953	. . . . . . 7 $/\$
14	11, 12, 13	sylancl 666	. . . . . 6 $/\$
15	14	rphalfcld 11360	. . . . 5 $/\$
16	2, 15	syl5eqel 2511	. . . 4 $/\$
17		simpr 462	. . . . 5 $/\$
18	16	rpreccld 11358	. . . . . 6 $/\$
19	18	rpred 11348	. . . . 5 $/\$
20	17, 19	rpcxpcld 23673	. . . 4 $/\$
21	16, 20	ifcld 3954	. . 3 $/\$
22	1, 21	syl5eqel 2511	. 2 $/\$
23		elrege0 11745	. . . 4 $/\$
24		0red 9651	. . . . . . 7 $/\$
25		leloe 9727	. . . . . . 7 $/\$ $\/$
26	24, 25	sylan 473	. . . . . 6 $/\$ $/\$ $\/$
27		elrp 11311	. . . . . . . . 9 $/\$
28		simp2l 1031	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
29		simp2r 1032	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
30		cnvimass 5207	. . . . . . . . . . . . . . . . . 18
31	5	fdmi 5751	. . . . . . . . . . . . . . . . . 18
32	30, 31	sseqtri 3496	. . . . . . . . . . . . . . . . 17
33	3, 32	eqsstri 3494	. . . . . . . . . . . . . . . 16
34	33	sseli 3460	. . . . . . . . . . . . . . 15
35	29, 34	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
36		abscxp 23635	. . . . . . . . . . . . . 14 $/\$
37	28, 35, 36	syl2anc 665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
38	35	recld 13257	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
39	28, 38	rpcxpcld 23673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	rpred 11348	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
41	16	3ad2ant1 1026	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
42	41	rpred 11348	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
43	28, 42	rpcxpcld 23673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44	43	rpred 11348	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
45		simp1r 1030	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
46	45	rpred 11348	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
47		simp1l 1029	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
48	9	simplbi 461	. . . . . . . . . . . . . . . . . . 19
49	47, 48	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
50	49	recld 13257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	rehalfcld 10866	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
52		1re 9649	. . . . . . . . . . . . . . . . . . 19
53		min1 11490	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancl 666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	14	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	rpred 11348	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
57		2re 10686	. . . . . . . . . . . . . . . . . . . 20
58	57	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
59		2pos 10708	. . . . . . . . . . . . . . . . . . . 20
60	59	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
61		lediv1 10477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
62	56, 50, 58, 60, 61	syl112anc 1268	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
63	54, 62	mpbid 213	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
64	2, 63	syl5eqbr 4457	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
65	50	recnd 9676	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	65	2halvesd 10865	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
67	49, 35	resubd 13279	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
68	49, 35	subcld 9993	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
69	68	recld 13257	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
70	68	abscld 13497	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
71	68	releabsd 13512	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
72		simp3r 1034	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
73	72, 1	syl6breq 4463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
74	20	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rpred 11348	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
76		ltmin 11495	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
77	70, 42, 75, 76	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	73, 77	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	simpld 460	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
80	69, 70, 42, 71, 79	lelttrd 9800	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
81	69, 42, 51, 80, 64	ltletrd 9802	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
82	67, 81	eqbrtrrd 4446	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
83	50, 38, 51	ltsubadd2d 10218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
84	82, 83	mpbid 213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
85	66, 84	eqbrtrd 4444	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
86	51, 38, 51	ltadd1d 10213	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
87	85, 86	mpbird 235	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
88	42, 51, 38, 64, 87	lelttrd 9800	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
89	28	rpred 11348	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
90	52	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
91	28	rprege0d 11355	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92		absid 13359	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
94		simp3l 1033	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
95	93, 94	eqbrtrrd 4446	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
96	95, 1	syl6breq 4463	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
97		ltmin 11495	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
98	89, 42, 75, 97	syl3anc 1264	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbid 213	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	simpld 460	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
101		rehalfcl 10846	. . . . . . . . . . . . . . . . . . 19
102	52, 101	mp1i 13	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
103		min2 11491	. . . . . . . . . . . . . . . . . . . . 21 $/\$
104	50, 52, 103	sylancl 666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
105		lediv1 10477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
106	56, 90, 58, 60, 105	syl112anc 1268	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
107	104, 106	mpbid 213	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
108	2, 107	syl5eqbr 4457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
109		halflt1 10838	. . . . . . . . . . . . . . . . . . 19
110	109	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	42, 102, 90, 108, 110	lelttrd 9800	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	89, 42, 90, 100, 111	lttrd 9803	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
113	28, 42, 112, 38	cxplt3d 23675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
114	88, 113	mpbid 213	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	41	rpcnne0d 11357	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		recid 10291	. . . . . . . . . . . . . . . . . . 19 $/\$
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
118	117	oveq2d 6321	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
119	41	rpreccld 11358	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
120	119	rpcnd 11350	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
121	28, 42, 120	cxpmuld 23677	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
122	28	rpcnd 11350	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
123	122	cxp1d 23649	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
124	118, 121, 123	3eqtr3d 2471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
125	99	simprd 464	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
126	124, 125	eqbrtrd 4444	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
127	43	rprege0d 11355	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	45	rprege0d 11355	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129		cxplt2 23641	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
130	127, 128, 119, 129	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
131	126, 130	mpbird 235	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
132	40, 44, 46, 114, 131	lttrd 9803	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
133	37, 132	eqbrtrd 4444	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
134	133	3expia 1207	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
135	134	anassrs 652	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
136	135	ralrimiva 2836	. . . . . . . . 9 $/\$ $/\$ $/\$
137	27, 136	sylan2br 478	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
138	137	expr 618	. . . . . . 7 $/\$ $/\$ $/\$
139		elpreima 6017	. . . . . . . . . . . . . . . . . . 19 $/\$
140	5, 6, 139	mp2b 10	. . . . . . . . . . . . . . . . . 18 $/\$
141	140	simprbi 465	. . . . . . . . . . . . . . . . 17
142	141, 3	eleq2s 2527	. . . . . . . . . . . . . . . 16
143	142	rpne0d 11353	. . . . . . . . . . . . . . 15
144		fveq2 5881	. . . . . . . . . . . . . . . . 17
145		re0 13215	. . . . . . . . . . . . . . . . 17
146	144, 145	syl6eq 2479	. . . . . . . . . . . . . . . 16
147	146	necon3i 2660	. . . . . . . . . . . . . . 15
148	143, 147	syl 17	. . . . . . . . . . . . . 14
149	34, 148	0cxpd 23653	. . . . . . . . . . . . 13
150	149	adantl 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	150	abs00bd 13354	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152		simpllr 767	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	152	rpgt0d 11351	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	151, 153	eqbrtrd 4444	. . . . . . . . . 10 $/\$ $/\$ $/\$
155		oveq1 6312	. . . . . . . . . . . 12
156	155	fveq2d 5885	. . . . . . . . . . 11
157	156	breq1d 4433	. . . . . . . . . 10
158	154, 157	syl5ibcom 223	. . . . . . . . 9 $/\$ $/\$ $/\$
159	158	a1dd 47	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
160	159	ralrimdva 2840	. . . . . . 7 $/\$ $/\$ $/\$
161	138, 160	jaod 381	. . . . . 6 $/\$ $/\$ $\/$ $/\$
162	26, 161	sylbid 218	. . . . 5 $/\$ $/\$ $/\$
163	162	expimpd 606	. . . 4 $/\$ $/\$ $/\$
164	23, 163	syl5bi 220	. . 3 $/\$ $/\$
165	164	ralrimiv 2834	. 2 $/\$ $/\$
166		breq2 4427	. . . . . 6
167		breq2 4427	. . . . . 6
168	166, 167	anbi12d 715	. . . . 5 $/\$ $/\$
169	168	imbi1d 318	. . . 4 $/\$ $/\$
170	169	2ralbidv 2866	. . 3 $/\$ $/\$
171	170	rspcev 3182	. 2 $/\$ $/\$ $/\$
172	22, 165, 171	syl2anc 665	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wne 2614

wral 2771

wrex 2772

cif 3911 class class class wbr 4423

ccnv 4852

cdm 4853

cima 4856

wfn 5596

wf 5597

cfv 5601 (class class class)co 6305

cc 9544

cr 9545

cc0 9546

c1 9547

caddc 9549

cmul 9551

cpnf 9679

clt 9682

cle 9683

cmin 9867

cdiv 10276

c2 10666

crp 11309

cico 11644

cre 13160

cabs 13297 ↾_t crest 15318

ctopn 15319 ℂ_fldccnfld 18969

ccxp 23503

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-inf2 8155 ax-cnex 9602 ax-resscn 9603 ax-1cn 9604 ax-icn 9605 ax-addcl 9606 ax-addrcl 9607 ax-mulcl 9608 ax-mulrcl 9609 ax-mulcom 9610 ax-addass 9611 ax-mulass 9612 ax-distr 9613 ax-i2m1 9614 ax-1ne0 9615 ax-1rid 9616 ax-rnegex 9617 ax-rrecex 9618 ax-cnre 9619 ax-pre-lttri 9620 ax-pre-lttrn 9621 ax-pre-ltadd 9622 ax-pre-mulgt0 9623 ax-pre-sup 9624 ax-addf 9625 ax-mulf 9626

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-iin 4302 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-of 6545 df-om 6707 df-1st 6807 df-2nd 6808 df-supp 6926 df-wrecs 7039 df-recs 7101 df-rdg 7139 df-1o 7193 df-2o 7194 df-oadd 7197 df-er 7374 df-map 7485 df-pm 7486 df-ixp 7534 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-fsupp 7893 df-fi 7934 df-sup 7965 df-inf 7966 df-oi 8034 df-card 8381 df-cda 8605 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-sub 9869 df-neg 9870 df-div 10277 df-nn 10617 df-2 10675 df-3 10676 df-4 10677 df-5 10678 df-6 10679 df-7 10680 df-8 10681 df-9 10682 df-10 10683 df-n0 10877 df-z 10945 df-dec 11059 df-uz 11167 df-q 11272 df-rp 11310 df-xneg 11416 df-xadd 11417 df-xmul 11418 df-ioo 11646 df-ioc 11647 df-ico 11648 df-icc 11649 df-fz 11792 df-fzo 11923 df-fl 12034 df-mod 12103 df-seq 12220 df-exp 12279 df-fac 12466 df-bc 12494 df-hash 12522 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13525 df-clim 13551 df-rlim 13552 df-sum 13752 df-ef 14120 df-sin 14122 df-cos 14123 df-pi 14125 df-struct 15122 df-ndx 15123 df-slot 15124 df-base 15125 df-sets 15126 df-ress 15127 df-plusg 15202 df-mulr 15203 df-starv 15204 df-sca 15205 df-vsca 15206 df-ip 15207 df-tset 15208 df-ple 15209 df-ds 15211 df-unif 15212 df-hom 15213 df-cco 15214 df-rest 15320 df-topn 15321 df-0g 15339 df-gsum 15340 df-topgen 15341 df-pt 15342 df-prds 15345 df-xrs 15399 df-qtop 15405 df-imas 15406 df-xps 15409 df-mre 15491 df-mrc 15492 df-acs 15494 df-mgm 16487 df-sgrp 16526 df-mnd 16536 df-submnd 16582 df-mulg 16675 df-cntz 16970 df-cmn 17431 df-psmet 18961 df-xmet 18962 df-met 18963 df-bl 18964 df-mopn 18965 df-fbas 18966 df-fg 18967 df-cnfld 18970 df-top 19919 df-bases 19920 df-topon 19921 df-topsp 19922 df-cld 20032 df-ntr 20033 df-cls 20034 df-nei 20112 df-lp 20150 df-perf 20151 df-cn 20241 df-cnp 20242 df-haus 20329 df-tx 20575 df-hmeo 20768 df-fil 20859 df-fm 20951 df-flim 20952 df-flf 20953 df-xms 21333 df-ms 21334 df-tms 21335 df-cncf 21908 df-limc 22819 df-dv 22820 df-log 23504 df-cxp 23505

This theorem is referenced by: cxpcn3 23686

W3C validator