cxpcn3lem - Metamath Proof Explorer

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

Theorem cxpcn3lem 23766

Description: Lemma for cxpcn3 23767. (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 2541	. . . . . . . . . 10
5		ref 13252	. . . . . . . . . . 11
6		ffn 5739	. . . . . . . . . . 11
7		elpreima 6017	. . . . . . . . . . 11 $/\$
8	5, 6, 7	mp2b 10	. . . . . . . . . 10 $/\$
9	4, 8	bitri 257	. . . . . . . . 9 $/\$
10	9	simprbi 471	. . . . . . . 8
11	10	adantr 472	. . . . . . 7 $/\$
12		1rp 11329	. . . . . . 7
13		ifcl 3914	. . . . . . 7 $/\$
14	11, 12, 13	sylancl 675	. . . . . 6 $/\$
15	14	rphalfcld 11376	. . . . 5 $/\$
16	2, 15	syl5eqel 2553	. . . 4 $/\$
17		simpr 468	. . . . 5 $/\$
18	16	rpreccld 11374	. . . . . 6 $/\$
19	18	rpred 11364	. . . . 5 $/\$
20	17, 19	rpcxpcld 23754	. . . 4 $/\$
21	16, 20	ifcld 3915	. . 3 $/\$
22	1, 21	syl5eqel 2553	. 2 $/\$
23		elrege0 11764	. . . 4 $/\$
24		0red 9662	. . . . . . 7 $/\$
25		leloe 9738	. . . . . . 7 $/\$ $\/$
26	24, 25	sylan 479	. . . . . 6 $/\$ $/\$ $\/$
27		elrp 11327	. . . . . . . . 9 $/\$
28		simp2l 1056	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
29		simp2r 1057	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
30		cnvimass 5194	. . . . . . . . . . . . . . . . . 18
31	5	fdmi 5746	. . . . . . . . . . . . . . . . . 18
32	30, 31	sseqtri 3450	. . . . . . . . . . . . . . . . 17
33	3, 32	eqsstri 3448	. . . . . . . . . . . . . . . 16
34	33	sseli 3414	. . . . . . . . . . . . . . 15
35	29, 34	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
36		abscxp 23716	. . . . . . . . . . . . . 14 $/\$
37	28, 35, 36	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
38	35	recld 13334	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
39	28, 38	rpcxpcld 23754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	rpred 11364	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
41	16	3ad2ant1 1051	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
42	41	rpred 11364	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
43	28, 42	rpcxpcld 23754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44	43	rpred 11364	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
45		simp1r 1055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
46	45	rpred 11364	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
47		simp1l 1054	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
48	9	simplbi 467	. . . . . . . . . . . . . . . . . . 19
49	47, 48	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
50	49	recld 13334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	rehalfcld 10882	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
52		1re 9660	. . . . . . . . . . . . . . . . . . 19
53		min1 11506	. . . . . . . . . . . . . . . . . . 19 $/\$
54	50, 52, 53	sylancl 675	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
55	14	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	rpred 11364	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
57		2re 10701	. . . . . . . . . . . . . . . . . . . 20
58	57	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
59		2pos 10723	. . . . . . . . . . . . . . . . . . . 20
60	59	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
61		lediv1 10492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
62	56, 50, 58, 60, 61	syl112anc 1296	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
63	54, 62	mpbid 215	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
64	2, 63	syl5eqbr 4429	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
65	50	recnd 9687	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
66	65	2halvesd 10881	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
67	49, 35	resubd 13356	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
68	49, 35	subcld 10005	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
69	68	recld 13334	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
70	68	abscld 13575	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
71	68	releabsd 13590	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
72		simp3r 1059	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
73	72, 1	syl6breq 4435	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
74	20	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rpred 11364	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
76		ltmin 11511	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
77	70, 42, 75, 76	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	73, 77	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	simpld 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
80	69, 70, 42, 71, 79	lelttrd 9810	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
81	69, 42, 51, 80, 64	ltletrd 9812	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
82	67, 81	eqbrtrrd 4418	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
83	50, 38, 51	ltsubadd2d 10232	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
84	82, 83	mpbid 215	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
85	66, 84	eqbrtrd 4416	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
86	51, 38, 51	ltadd1d 10227	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
87	85, 86	mpbird 240	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
88	42, 51, 38, 64, 87	lelttrd 9810	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
89	28	rpred 11364	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
90	52	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
91	28	rprege0d 11371	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92		absid 13436	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
94		simp3l 1058	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
95	93, 94	eqbrtrrd 4418	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
96	95, 1	syl6breq 4435	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
97		ltmin 11511	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
98	89, 42, 75, 97	syl3anc 1292	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	96, 98	mpbid 215	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	simpld 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
101		rehalfcl 10862	. . . . . . . . . . . . . . . . . . 19
102	52, 101	mp1i 13	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
103		min2 11507	. . . . . . . . . . . . . . . . . . . . 21 $/\$
104	50, 52, 103	sylancl 675	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
105		lediv1 10492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
106	56, 90, 58, 60, 105	syl112anc 1296	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
107	104, 106	mpbid 215	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
108	2, 107	syl5eqbr 4429	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
109		halflt1 10854	. . . . . . . . . . . . . . . . . . 19
110	109	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111	42, 102, 90, 108, 110	lelttrd 9810	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
112	89, 42, 90, 100, 111	lttrd 9813	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
113	28, 42, 112, 38	cxplt3d 23756	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
114	88, 113	mpbid 215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	41	rpcnne0d 11373	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		recid 10306	. . . . . . . . . . . . . . . . . . 19 $/\$
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
118	117	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
119	41	rpreccld 11374	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
120	119	rpcnd 11366	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
121	28, 42, 120	cxpmuld 23758	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
122	28	rpcnd 11366	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
123	122	cxp1d 23730	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
124	118, 121, 123	3eqtr3d 2513	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
125	99	simprd 470	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
126	124, 125	eqbrtrd 4416	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
127	43	rprege0d 11371	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	45	rprege0d 11371	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129		cxplt2 23722	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
130	127, 128, 119, 129	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
131	126, 130	mpbird 240	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
132	40, 44, 46, 114, 131	lttrd 9813	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
133	37, 132	eqbrtrd 4416	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
134	133	3expia 1233	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
135	134	anassrs 660	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
136	135	ralrimiva 2809	. . . . . . . . 9 $/\$ $/\$ $/\$
137	27, 136	sylan2br 484	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
138	137	expr 626	. . . . . . 7 $/\$ $/\$ $/\$
139		elpreima 6017	. . . . . . . . . . . . . . . . . . 19 $/\$
140	5, 6, 139	mp2b 10	. . . . . . . . . . . . . . . . . 18 $/\$
141	140	simprbi 471	. . . . . . . . . . . . . . . . 17
142	141, 3	eleq2s 2567	. . . . . . . . . . . . . . . 16
143	142	rpne0d 11369	. . . . . . . . . . . . . . 15
144		fveq2 5879	. . . . . . . . . . . . . . . . 17
145		re0 13292	. . . . . . . . . . . . . . . . 17
146	144, 145	syl6eq 2521	. . . . . . . . . . . . . . . 16
147	146	necon3i 2675	. . . . . . . . . . . . . . 15
148	143, 147	syl 17	. . . . . . . . . . . . . 14
149	34, 148	0cxpd 23734	. . . . . . . . . . . . 13
150	149	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	150	abs00bd 13431	. . . . . . . . . . 11 $/\$ $/\$ $/\$
152		simpllr 777	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	152	rpgt0d 11367	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	151, 153	eqbrtrd 4416	. . . . . . . . . 10 $/\$ $/\$ $/\$
155		oveq1 6315	. . . . . . . . . . . 12
156	155	fveq2d 5883	. . . . . . . . . . 11
157	156	breq1d 4405	. . . . . . . . . 10
158	154, 157	syl5ibcom 228	. . . . . . . . 9 $/\$ $/\$ $/\$
159	158	a1dd 46	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
160	159	ralrimdva 2812	. . . . . . 7 $/\$ $/\$ $/\$
161	138, 160	jaod 387	. . . . . 6 $/\$ $/\$ $\/$ $/\$
162	26, 161	sylbid 223	. . . . 5 $/\$ $/\$ $/\$
163	162	expimpd 614	. . . 4 $/\$ $/\$ $/\$
164	23, 163	syl5bi 225	. . 3 $/\$ $/\$
165	164	ralrimiv 2808	. 2 $/\$ $/\$
166		breq2 4399	. . . . . 6
167		breq2 4399	. . . . . 6
168	166, 167	anbi12d 725	. . . . 5 $/\$ $/\$
169	168	imbi1d 324	. . . 4 $/\$ $/\$
170	169	2ralbidv 2832	. . 3 $/\$ $/\$
171	170	rspcev 3136	. 2 $/\$ $/\$ $/\$
172	22, 165, 171	syl2anc 673	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cif 3872 class class class wbr 4395

ccnv 4838

cdm 4839

cima 4842

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cpnf 9690

clt 9693

cle 9694

cmin 9880

cdiv 10291

c2 10681

crp 11325

cico 11662

cre 13237

cabs 13374 ↾_t crest 15397

ctopn 15398 ℂ_fldccnfld 19047

ccxp 23584

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cxp 23586

This theorem is referenced by: cxpcn3 23767

W3C validator