bddmulibl - Metamath Proof Explorer

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

Theorem bddmulibl 19683

Description: A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)

**Assertion**
Ref	Expression
bddmulibl	MblFn $/\$ $/\$

Distinct variable groups:

Proof of Theorem bddmulibl Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbff 19472	. . . . . . 7 MblFn
2	1	ad2antrr 707	. . . . . 6 MblFn $/\$ $/\$ $/\$
3		ffn 5550	. . . . . 6
4	2, 3	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
5		iblmbf 19612	. . . . . . . 8 MblFn
6	5	ad2antlr 708	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
7		mbff 19472	. . . . . . 7 MblFn
8	6, 7	syl 16	. . . . . 6 MblFn $/\$ $/\$ $/\$
9		ffn 5550	. . . . . 6
10	8, 9	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
11		mbfdm 19473	. . . . . 6 MblFn
12	11	ad2antrr 707	. . . . 5 MblFn $/\$ $/\$ $/\$
13		mbfdm 19473	. . . . . 6 MblFn
14	6, 13	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
15		eqid 2404	. . . . 5
16		eqidd 2405	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
17		eqidd 2405	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
18	4, 10, 12, 14, 15, 16, 17	offval 6271	. . . 4 MblFn $/\$ $/\$ $/\$
19		ovex 6065	. . . . . 6
20	19	a1i 11	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
21		simpll 731	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
22	21, 6	mbfmul 19571	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
23	18, 22	eqeltrrd 2479	. . . . 5 MblFn $/\$ $/\$ $/\$ MblFn
24	23, 20	mbfmptcl 19482	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
25		eqidd 2405	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
26		absf 12096	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
28	27	feqmptd 5738	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
29		fveq2 5687	. . . . . . . 8
30	24, 25, 28, 29	fmptco 5860	. . . . . . 7 MblFn $/\$ $/\$ $/\$
31		eqid 2404	. . . . . . . . 9
32	24, 31	fmptd 5852	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
33		ax-resscn 9003	. . . . . . . . . . 11
34		ssid 3327	. . . . . . . . . . 11
35		cncfss 18882	. . . . . . . . . . 11 $/\$
36	33, 34, 35	mp2an 654	. . . . . . . . . 10
37		abscncf 18884	. . . . . . . . . 10
38	36, 37	sselii 3305	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
40		cncombf 19503	. . . . . . . 8 MblFn $/\$ $/\$ MblFn
41	23, 32, 39, 40	syl3anc 1184	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
42	30, 41	eqeltrrd 2479	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
43	24	abscld 12193	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
44	43	rexrd 9090	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
45	24	absge0d 12201	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
46		elxrge0 10964	. . . . . . . . . . 11 $/\$
47	44, 45, 46	sylanbrc 646	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
48		0xr 9087	. . . . . . . . . . . 12
49		0le0 10037	. . . . . . . . . . . 12
50		elxrge0 10964	. . . . . . . . . . . 12 $/\$
51	48, 49, 50	mpbir2an 887	. . . . . . . . . . 11
52	51	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
53	47, 52	ifclda 3726	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
54	53	adantr 452	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
55		eqid 2404	. . . . . . . 8
56	54, 55	fmptd 5852	. . . . . . 7 MblFn $/\$ $/\$ $/\$
57		reex 9037	. . . . . . . . . . . . . . 15
58	57	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
59		simprl 733	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
60	59	ad2antrr 707	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
61		elin 3490	. . . . . . . . . . . . . . . . . . . 20 $/\$
62	61	simprbi 451	. . . . . . . . . . . . . . . . . . 19
63		ffvelrn 5827	. . . . . . . . . . . . . . . . . . 19 $/\$
64	8, 62, 63	syl2an 464	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
65	64	abscld 12193	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
66	64	absge0d 12201	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
67		elrege0 10963	. . . . . . . . . . . . . . . . 17 $/\$
68	65, 66, 67	sylanbrc 646	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
69		0re 9047	. . . . . . . . . . . . . . . . . 18
70		elrege0 10963	. . . . . . . . . . . . . . . . . 18 $/\$
71	69, 49, 70	mpbir2an 887	. . . . . . . . . . . . . . . . 17
72	71	a1i 11	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
73	68, 72	ifclda 3726	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
74	73	ad2antrr 707	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
75		fconstmpt 4880	. . . . . . . . . . . . . . 15
76	75	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
77		eqidd 2405	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
78	58, 60, 74, 76, 77	offval2 6281	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
79		oveq2 6048	. . . . . . . . . . . . . . . 16
80		oveq2 6048	. . . . . . . . . . . . . . . 16
81	79, 80	ifsb 3708	. . . . . . . . . . . . . . 15
82	59	recnd 9070	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
83	82	adantr 452	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
84	83	mul01d 9221	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
85	84	ifeq2d 3714	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ $/\$
86	81, 85	syl5eq 2448	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
87	86	mpteq2dv 4256	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
88	78, 87	eqtrd 2436	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
89	88	fveq2d 5691	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
90	73	adantr 452	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
91		eqid 2404	. . . . . . . . . . . . . 14
92	90, 91	fmptd 5852	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
93	92	adantr 452	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
94		inss2 3522	. . . . . . . . . . . . . . . . . 18
95	94	a1i 11	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
96	23, 20	mbfdm2 19483	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
97	8	ffvelrnda 5829	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
98	8	feqmptd 5738	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
99		simplr 732	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
100	98, 99	eqeltrrd 2479	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
101	95, 96, 97, 100	iblss 19649	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
102	64, 101	iblabs 19673	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
103	65, 66	iblpos 19637	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ MblFn $/\$
104	102, 103	mpbid 202	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ MblFn $/\$
105	104	simprd 450	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
106	105	adantr 452	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
107		simplrl 737	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
108		neq0 3598	. . . . . . . . . . . . . . 15
109	69	a1i 11	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
110	61	simplbi 447	. . . . . . . . . . . . . . . . . . . 20
111		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . 20 $/\$
112	2, 110, 111	syl2an 464	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$ $/\$
113	112	abscld 12193	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
114		simplrl 737	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
115	112	absge0d 12201	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
116		simprr 734	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$
117		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . 22
118	117	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . 21
119	118	breq1d 4182	. . . . . . . . . . . . . . . . . . . 20
120	119	rspccva 3011	. . . . . . . . . . . . . . . . . . 19 $/\$
121	116, 110, 120	syl2an 464	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
122	109, 113, 114, 115, 121	letrd 9183	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
123	122	ex 424	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
124	123	exlimdv 1643	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
125	108, 124	syl5bi 209	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$
126	125	imp 419	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
127		elrege0 10963	. . . . . . . . . . . . 13 $/\$
128	107, 126, 127	sylanbrc 646	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
129	93, 106, 128	itg2mulc 19592	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
130	89, 129	eqtr3d 2438	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
131	107, 106	remulcld 9072	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
132	130, 131	eqeltrd 2478	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
133	132	ex 424	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
134		noel 3592	. . . . . . . . . . . . . 14
135		eleq2 2465	. . . . . . . . . . . . . 14
136	134, 135	mtbiri 295	. . . . . . . . . . . . 13
137		iffalse 3706	. . . . . . . . . . . . 13
138	136, 137	syl 16	. . . . . . . . . . . 12
139	138	mpteq2dv 4256	. . . . . . . . . . 11
140		fconstmpt 4880	. . . . . . . . . . 11
141	139, 140	syl6eqr 2454	. . . . . . . . . 10
142	141	fveq2d 5691	. . . . . . . . 9
143		itg20 19582	. . . . . . . . . 10
144	143, 69	eqeltri 2474	. . . . . . . . 9
145	142, 144	syl6eqel 2492	. . . . . . . 8
146	133, 145	pm2.61d2 154	. . . . . . 7 MblFn $/\$ $/\$ $/\$
147	114, 65	remulcld 9072	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
148	147	rexrd 9090	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
149	114, 65, 122, 66	mulge0d 9559	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
150		elxrge0 10964	. . . . . . . . . . . 12 $/\$
151	148, 149, 150	sylanbrc 646	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
152	151, 52	ifclda 3726	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
153	152	adantr 452	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
154		eqid 2404	. . . . . . . . 9
155	153, 154	fmptd 5852	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
156	112, 64	absmuld 12211	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
157		abscl 12038	. . . . . . . . . . . . . . . 16
158		absge0 12047	. . . . . . . . . . . . . . . 16
159	157, 158	jca 519	. . . . . . . . . . . . . . 15 $/\$
160	64, 159	syl 16	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
161		lemul1a 9820	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
162	113, 114, 160, 121, 161	syl31anc 1187	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
163	156, 162	eqbrtrd 4192	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
164		iftrue 3705	. . . . . . . . . . . . 13
165	164	adantl 453	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
166		iftrue 3705	. . . . . . . . . . . . 13
167	166	adantl 453	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
168	163, 165, 167	3brtr4d 4202	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
169	49	a1i 11	. . . . . . . . . . . . 13
170		iffalse 3706	. . . . . . . . . . . . 13
171	169, 170, 137	3brtr4d 4202	. . . . . . . . . . . 12
172	171	adantl 453	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
173	168, 172	pm2.61dan 767	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
174	173	ralrimivw 2750	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
175	57	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
176		eqidd 2405	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
177		eqidd 2405	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
178	175, 54, 153, 176, 177	ofrfval2 6282	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
179	174, 178	mpbird 224	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
180		itg2le 19584	. . . . . . . 8 $/\$ $/\$
181	56, 155, 179, 180	syl3anc 1184	. . . . . . 7 MblFn $/\$ $/\$ $/\$
182		itg2lecl 19583	. . . . . . 7 $/\$ $/\$
183	56, 146, 181, 182	syl3anc 1184	. . . . . 6 MblFn $/\$ $/\$ $/\$
184	43, 45	iblpos 19637	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn $/\$
185	42, 183, 184	mpbir2and 889	. . . . 5 MblFn $/\$ $/\$ $/\$
186	20, 23, 185	iblabsr 19674	. . . 4 MblFn $/\$ $/\$ $/\$
187	18, 186	eqeltrd 2478	. . 3 MblFn $/\$ $/\$ $/\$
188	187	rexlimdvaa 2791	. 2 MblFn $/\$
189	188	3impia 1150	1 MblFn $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 359 $/\$ w3a 936

wex 1547

wceq 1649

wcel 1721

wral 2666

wrex 2667

cvv 2916

cin 3279

wss 3280

c0 3588

cif 3699

csn 3774 class class class wbr 4172

cmpt 4226

cxp 4835

cdm 4837

ccom 4841

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cof 6262

cofr 6263

cc 8944

cr 8945

cc0 8946

cmul 8951

cpnf 9073

cxr 9075

cle 9077

cico 10874

cicc 10875

cabs 11994

ccncf 18859

cvol 19313 MblFncmbf 19459

citg2 19461

cibl 19462

This theorem is referenced by: bddibl 19684 itgsubstlem 19885

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-cc 8271 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-disj 4143 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-ofr 6265 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-omul 6688 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-acn 7785 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-hash 11574 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-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-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cn 17245 df-cnp 17246 df-cmp 17404 df-tx 17547 df-hmeo 17740 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-ovol 19314 df-vol 19315 df-mbf 19465 df-itg1 19466 df-itg2 19467 df-ibl 19468 df-0p 19515

W3C validator