carsgclctunlem2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > carsgclctunlem2		Structured version Visualization version Unicode version

Theorem carsgclctunlem2 29224

Description: Lemma for carsgclctun 29226. (Contributed by Thierry Arnoux, 25-May-2020.)

**Hypotheses**
Ref	Expression
carsgval.1
carsgval.2
carsgsiga.1
carsgsiga.2	$/\$ $/\$ Σ^*
carsgsiga.3	$/\$ $/\$
carsgclctunlem2.1	Disj
carsgclctunlem2.2	$/\$ toCaraSiga
carsgclctunlem2.3
carsgclctunlem2.4

**Assertion**
Ref	Expression
carsgclctunlem2	$\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem carsgclctunlem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iunin2 4333	. . . . 5
2	1	fveq2i 5882	. . . 4
3		iccssxr 11742	. . . . 5
4		carsgval.2	. . . . . 6
5		nnex 10637	. . . . . . . 8
6	5	a1i 11	. . . . . . 7
7		carsgclctunlem2.3	. . . . . . . . 9
8	7	adantr 472	. . . . . . . 8 $/\$
9	8	elpwincl1 28232	. . . . . . 7 $/\$
10	6, 9	elpwiuncl 28234	. . . . . 6
11	4, 10	ffvelrnd 6038	. . . . 5
12	3, 11	sseldi 3416	. . . 4
13	2, 12	syl5eqelr 2554	. . 3
14	4, 7	ffvelrnd 6038	. . . . 5
15	3, 14	sseldi 3416	. . . 4
16	7	elpwdifcl 28233	. . . . . . 7 $\$
17	4, 16	ffvelrnd 6038	. . . . . 6 $\$
18	3, 17	sseldi 3416	. . . . 5 $\$
19	18	xnegcld 11611	. . . 4 $\$
20	15, 19	xaddcld 11612	. . 3 $\$
21	4	adantr 472	. . . . . . . . 9 $/\$
22	21, 9	ffvelrnd 6038	. . . . . . . 8 $/\$
23	22	ralrimiva 2809	. . . . . . 7
24		nfcv 2612	. . . . . . . 8
25	24	esumcl 28925	. . . . . . 7 $/\$ Σ^*
26	6, 23, 25	syl2anc 673	. . . . . 6 Σ^*
27	3, 26	sseldi 3416	. . . . 5 Σ^*
28	9	ralrimiva 2809	. . . . . . . . 9
29		dfiun3g 5093	. . . . . . . . 9
30	28, 29	syl 17	. . . . . . . 8
31	30	fveq2d 5883	. . . . . . 7
32		nnct 28369	. . . . . . . . . 10
33		mptct 28377	. . . . . . . . . 10
34		rnct 28375	. . . . . . . . . 10
35	32, 33, 34	mp2b 10	. . . . . . . . 9
36	35	a1i 11	. . . . . . . 8
37		eqid 2471	. . . . . . . . . 10
38	37	rnmptss 6068	. . . . . . . . 9
39	28, 38	syl 17	. . . . . . . 8
40		mptexg 6151	. . . . . . . . . 10
41		rnexg 6744	. . . . . . . . . 10
42	5, 40, 41	mp2b 10	. . . . . . . . 9
43		breq1 4398	. . . . . . . . . . . 12
44		sseq1 3439	. . . . . . . . . . . 12
45	43, 44	3anbi23d 1368	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
46		unieq 4198	. . . . . . . . . . . . 13
47	46	fveq2d 5883	. . . . . . . . . . . 12
48		esumeq1 28929	. . . . . . . . . . . 12 Σ^* Σ^*
49	47, 48	breq12d 4408	. . . . . . . . . . 11 Σ^* Σ^*
50	45, 49	imbi12d 327	. . . . . . . . . 10 $/\$ $/\$ Σ^* $/\$ $/\$ Σ^*
51		carsgsiga.2	. . . . . . . . . 10 $/\$ $/\$ Σ^*
52	50, 51	vtoclg 3093	. . . . . . . . 9 $/\$ $/\$ Σ^*
53	42, 52	ax-mp 5	. . . . . . . 8 $/\$ $/\$ Σ^*
54	36, 39, 53	mpd3an23 1392	. . . . . . 7 Σ^*
55	31, 54	eqbrtrd 4416	. . . . . 6 Σ^*
56		fveq2 5879	. . . . . . 7
57		simpr 468	. . . . . . . . 9 $/\$ $/\$
58	57	fveq2d 5883	. . . . . . . 8 $/\$ $/\$
59		carsgsiga.1	. . . . . . . . 9
60	59	ad2antrr 740	. . . . . . . 8 $/\$ $/\$
61	58, 60	eqtrd 2505	. . . . . . 7 $/\$ $/\$
62		carsgclctunlem2.1	. . . . . . . . 9 Disj
63		disjin 28273	. . . . . . . . 9 Disj Disj
64	62, 63	syl 17	. . . . . . . 8 Disj
65		incom 3616	. . . . . . . . . 10
66	65	rgenw 2768	. . . . . . . . 9
67		disjeq2 4370	. . . . . . . . 9 Disj Disj
68	66, 67	ax-mp 5	. . . . . . . 8 Disj Disj
69	64, 68	sylib 201	. . . . . . 7 Disj
70	56, 6, 22, 9, 61, 69	esumrnmpt2 28963	. . . . . 6 Σ^* Σ^*
71	55, 70	breqtrd 4420	. . . . 5 Σ^*
72		carsgval.1	. . . . . . . 8
73		difssd 3550	. . . . . . . 8 $\$
74		carsgsiga.3	. . . . . . . 8 $/\$ $/\$
75	72, 4, 73, 7, 74	carsgmon 29219	. . . . . . 7 $\$
76	14, 17, 75	xrge0subcld 28420	. . . . . 6 $\$
77	4	adantr 472	. . . . . . . . . . . 12 $/\$
78	7	adantr 472	. . . . . . . . . . . . 13 $/\$
79	78	elpwincl1 28232	. . . . . . . . . . . 12 $/\$
80	77, 79	ffvelrnd 6038	. . . . . . . . . . 11 $/\$
81	3, 80	sseldi 3416	. . . . . . . . . 10 $/\$
82		xrge0neqmnf 11762	. . . . . . . . . . 11
83	80, 82	syl 17	. . . . . . . . . 10 $/\$
84	78	elpwdifcl 28233	. . . . . . . . . . . 12 $/\$ $\$
85	77, 84	ffvelrnd 6038	. . . . . . . . . . 11 $/\$ $\$
86	3, 85	sseldi 3416	. . . . . . . . . 10 $/\$ $\$
87		xrge0neqmnf 11762	. . . . . . . . . . 11 $\$ $\$
88	85, 87	syl 17	. . . . . . . . . 10 $/\$ $\$
89	86	xnegcld 11611	. . . . . . . . . 10 $/\$ $\$
90		xnegneg 11530	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
91	86, 90	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $\$ $\$
92	91	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$ $\$
93		xnegeq 11523	. . . . . . . . . . . . . . . . 17 $\$ $\$
94	93	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
95		xnegmnf 11526	. . . . . . . . . . . . . . . 16
96	94, 95	syl6eq 2521	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
97	92, 96	eqtr3d 2507	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
98	97	oveq2d 6324	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
99		simpll 768	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
100		fz1ssnn 11856	. . . . . . . . . . . . . . . . . . . . . . 23
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
102	101	sselda 3418	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103		carsgclctunlem2.2	. . . . . . . . . . . . . . . . . . . . 21 $/\$ toCaraSiga
104	99, 102, 103	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ toCaraSiga
105	104	ralrimiva 2809	. . . . . . . . . . . . . . . . . . 19 $/\$ toCaraSiga
106		dfiun3g 5093	. . . . . . . . . . . . . . . . . . 19 toCaraSiga
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
108	72	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
109	59	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$
110	51	3adant1r 1285	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ Σ^*
111		fzfi 12223	. . . . . . . . . . . . . . . . . . . . 21
112		mptfi 7891	. . . . . . . . . . . . . . . . . . . . 21
113		rnfi 7875	. . . . . . . . . . . . . . . . . . . . 21
114	111, 112, 113	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
115	114	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
116		eqid 2471	. . . . . . . . . . . . . . . . . . . . 21
117	116	rnmptss 6068	. . . . . . . . . . . . . . . . . . . 20 toCaraSiga toCaraSiga
118	105, 117	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ toCaraSiga
119	108, 77, 109, 110, 115, 118	fiunelcarsg 29221	. . . . . . . . . . . . . . . . . 18 $/\$ toCaraSiga
120	107, 119	eqeltrd 2549	. . . . . . . . . . . . . . . . 17 $/\$ toCaraSiga
121	108, 77	elcarsg 29210	. . . . . . . . . . . . . . . . 17 $/\$ toCaraSiga $/\$ $\$
122	120, 121	mpbid 215	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
123	122	simprd 470	. . . . . . . . . . . . . . 15 $/\$ $\$
124		ineq1 3618	. . . . . . . . . . . . . . . . . . 19
125	124	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
126		difeq1 3533	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
127	126	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 $\$ $\$
128	125, 127	oveq12d 6326	. . . . . . . . . . . . . . . . 17 $\$ $\$
129		fveq2 5879	. . . . . . . . . . . . . . . . 17
130	128, 129	eqeq12d 2486	. . . . . . . . . . . . . . . 16 $\$ $\$
131	130	rspcv 3132	. . . . . . . . . . . . . . 15 $\$ $\$
132	78, 123, 131	sylc 61	. . . . . . . . . . . . . 14 $/\$ $\$
133	132	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
134		xaddpnf1 11542	. . . . . . . . . . . . . . 15 $/\$
135	81, 83, 134	syl2anc 673	. . . . . . . . . . . . . 14 $/\$
136	135	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
137	98, 133, 136	3eqtr3d 2513	. . . . . . . . . . . 12 $/\$ $/\$ $\$
138		carsgclctunlem2.4	. . . . . . . . . . . . . 14
139	138	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
140	139	neneqd 2648	. . . . . . . . . . . 12 $/\$ $/\$ $\$
141	137, 140	pm2.65da 586	. . . . . . . . . . 11 $/\$ $\$
142	141	neqned 2650	. . . . . . . . . 10 $/\$ $\$
143		xaddass 11560	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	81, 83, 86, 88, 89, 142, 143	syl222anc 1308	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$
145		xnegid 11553	. . . . . . . . . . 11 $\$ $\$ $\$
146	86, 145	syl 17	. . . . . . . . . 10 $/\$ $\$ $\$
147	146	oveq2d 6324	. . . . . . . . 9 $/\$ $\$ $\$
148		xaddid1 11556	. . . . . . . . . 10
149	81, 148	syl 17	. . . . . . . . 9 $/\$
150	144, 147, 149	3eqtrd 2509	. . . . . . . 8 $/\$ $\$ $\$
151	132	oveq1d 6323	. . . . . . . 8 $/\$ $\$ $\$ $\$
152	107	ineq2d 3625	. . . . . . . . . 10 $/\$
153	152	fveq2d 5883	. . . . . . . . 9 $/\$
154		fmptss 28352	. . . . . . . . . . . . 13
155		rnss 5069	. . . . . . . . . . . . 13
156	100, 154, 155	mp2b 10	. . . . . . . . . . . 12
157	156	a1i 11	. . . . . . . . . . 11 $/\$
158		disjrnmpt 28272	. . . . . . . . . . . . 13 Disj Disj
159	62, 158	syl 17	. . . . . . . . . . . 12 Disj
160	159	adantr 472	. . . . . . . . . . 11 $/\$ Disj
161		disjss1 4372	. . . . . . . . . . 11 Disj Disj
162	157, 160, 161	sylc 61	. . . . . . . . . 10 $/\$ Disj
163	108, 77, 109, 110, 115, 118, 162, 78	carsgclctunlem1 29222	. . . . . . . . 9 $/\$ Σ^*
164		ineq2 3619	. . . . . . . . . . 11
165	164	fveq2d 5883	. . . . . . . . . 10
166	111	elexi 3041	. . . . . . . . . . 11
167	166	a1i 11	. . . . . . . . . 10 $/\$
168	99, 102, 22	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$
169		inss2 3644	. . . . . . . . . . . . . . 15
170		sseq2 3440	. . . . . . . . . . . . . . 15
171	169, 170	mpbii 216	. . . . . . . . . . . . . 14
172		ss0 3768	. . . . . . . . . . . . . 14
173	171, 172	syl 17	. . . . . . . . . . . . 13
174	173	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
175	174	fveq2d 5883	. . . . . . . . . . 11 $/\$ $/\$ $/\$
176	109	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$
177	175, 176	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $/\$
178	62	adantr 472	. . . . . . . . . . 11 $/\$ Disj
179		disjss1 4372	. . . . . . . . . . 11 Disj Disj
180	101, 178, 179	sylc 61	. . . . . . . . . 10 $/\$ Disj
181	165, 167, 168, 104, 177, 180	esumrnmpt2 28963	. . . . . . . . 9 $/\$ Σ^* Σ^*
182	153, 163, 181	3eqtrd 2509	. . . . . . . 8 $/\$ Σ^*
183	150, 151, 182	3eqtr3rd 2514	. . . . . . 7 $/\$ Σ^* $\$
184	17	adantr 472	. . . . . . . . . 10 $/\$ $\$
185	3, 184	sseldi 3416	. . . . . . . . 9 $/\$ $\$
186	185	xnegcld 11611	. . . . . . . 8 $/\$ $\$
187	15	adantr 472	. . . . . . . 8 $/\$
188		iunss1 4281	. . . . . . . . . . . 12
189	100, 188	mp1i 13	. . . . . . . . . . 11 $/\$
190	189	sscond 3559	. . . . . . . . . 10 $/\$ $\$ $\$
191	74	3adant1r 1285	. . . . . . . . . 10 $/\$ $/\$ $/\$
192	108, 77, 190, 84, 191	carsgmon 29219	. . . . . . . . 9 $/\$ $\$ $\$
193		xleneg 11534	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
194	193	biimpa 492	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
195	185, 86, 192, 194	syl21anc 1291	. . . . . . . 8 $/\$ $\$ $\$
196		xleadd2a 11565	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
197	89, 186, 187, 195, 196	syl31anc 1295	. . . . . . 7 $/\$ $\$ $\$
198	183, 197	eqbrtrd 4416	. . . . . 6 $/\$ Σ^* $\$
199	76, 22, 198	esumgect 28985	. . . . 5 Σ^* $\$
200	12, 27, 20, 71, 199	xrletrd 11482	. . . 4 $\$
201	2, 200	syl5eqbrr 4430	. . 3 $\$
202		xleadd1a 11564	. . 3 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
203	13, 20, 18, 201, 202	syl31anc 1295	. 2 $\$ $\$ $\$
204		xrge0npcan 28531	. . 3 $/\$ $\$ $/\$ $\$ $\$ $\$
205	14, 17, 75, 204	syl3anc 1292	. 2 $\$ $\$
206	203, 205	breqtrd 4420	1 $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1452

wcel 1904

wne 2641

wral 2756

cvv 3031 $\$ cdif 3387

cin 3389

wss 3390

c0 3722

cpw 3942

cuni 4190

ciun 4269 Disj wdisj 4366 class class class wbr 4395

cmpt 4454

crn 4840

wf 5585

cfv 5589 (class class class)co 6308

com 6711

cdom 7585

cfn 7587

cc0 9557

c1 9558

cpnf 9690

cmnf 9691

cxr 9692

cle 9694

cn 10631

cxne 11429

cxad 11430

cicc 11663

cfz 11810 Σ^*cesum 28922 toCaraSigaccarsg 29206

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-ac2 8911 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-disj 4367 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-acn 8394 df-ac 8565 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-ordt 15477 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-ps 16524 df-tsr 16525 df-plusf 16565 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-mhm 16660 df-submnd 16661 df-grp 16751 df-minusg 16752 df-sbg 16753 df-mulg 16754 df-subg 16892 df-cntz 17049 df-cmn 17510 df-abl 17511 df-mgp 17802 df-ur 17814 df-ring 17860 df-cring 17861 df-subrg 18084 df-abv 18123 df-lmod 18171 df-scaf 18172 df-sra 18473 df-rgmod 18474 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-tmd 21165 df-tgp 21166 df-tsms 21219 df-trg 21252 df-xms 21413 df-ms 21414 df-tms 21415 df-nm 21675 df-ngp 21676 df-nrg 21678 df-nlm 21679 df-ii 21987 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-esum 28923 df-carsg 29207

This theorem is referenced by: carsgclctunlem3 29225

W3C validator