bddmulibl - Metamath Proof Explorer

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

Theorem bddmulibl 21296

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 21085	. . . . . . 7 MblFn
2	1	ad2antrr 725	. . . . . 6 MblFn $/\$ $/\$ $/\$
3		ffn 5554	. . . . . 6
4	2, 3	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
5		iblmbf 21225	. . . . . . . 8 MblFn
6	5	ad2antlr 726	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
7		mbff 21085	. . . . . . 7 MblFn
8	6, 7	syl 16	. . . . . 6 MblFn $/\$ $/\$ $/\$
9		ffn 5554	. . . . . 6
10	8, 9	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
11		mbfdm 21086	. . . . . 6 MblFn
12	11	ad2antrr 725	. . . . 5 MblFn $/\$ $/\$ $/\$
13		mbfdm 21086	. . . . . 6 MblFn
14	6, 13	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
15		eqid 2438	. . . . 5
16		eqidd 2439	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
17		eqidd 2439	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
18	4, 10, 12, 14, 15, 16, 17	offval 6322	. . . 4 MblFn $/\$ $/\$ $/\$
19		ovex 6111	. . . . . 6
20	19	a1i 11	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
21		simpll 753	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
22	21, 6	mbfmul 21184	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
23	18, 22	eqeltrrd 2513	. . . . 5 MblFn $/\$ $/\$ $/\$ MblFn
24	23, 20	mbfmptcl 21095	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
25		eqidd 2439	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
26		absf 12817	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
28	27	feqmptd 5739	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
29		fveq2 5686	. . . . . . . 8
30	24, 25, 28, 29	fmptco 5871	. . . . . . 7 MblFn $/\$ $/\$ $/\$
31		eqid 2438	. . . . . . . . 9
32	24, 31	fmptd 5862	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
33		ax-resscn 9331	. . . . . . . . . . 11
34		ssid 3370	. . . . . . . . . . 11
35		cncfss 20455	. . . . . . . . . . 11 $/\$
36	33, 34, 35	mp2an 672	. . . . . . . . . 10
37		abscncf 20457	. . . . . . . . . 10
38	36, 37	sselii 3348	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
40		cncombf 21116	. . . . . . . 8 MblFn $/\$ $/\$ MblFn
41	23, 32, 39, 40	syl3anc 1218	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
42	30, 41	eqeltrrd 2513	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
43	24	abscld 12914	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
44	43	rexrd 9425	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
45	24	absge0d 12922	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
46		elxrge0 11386	. . . . . . . . . . 11 $/\$
47	44, 45, 46	sylanbrc 664	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
48		0e0iccpnf 11388	. . . . . . . . . . 11
49	48	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
50	47, 49	ifclda 3816	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
51	50	adantr 465	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
52		eqid 2438	. . . . . . . 8
53	51, 52	fmptd 5862	. . . . . . 7 MblFn $/\$ $/\$ $/\$
54		reex 9365	. . . . . . . . . . . . . . 15
55	54	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
56		simprl 755	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
57	56	ad2antrr 725	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
58		elin 3534	. . . . . . . . . . . . . . . . . . . 20 $/\$
59	58	simprbi 464	. . . . . . . . . . . . . . . . . . 19
60		ffvelrn 5836	. . . . . . . . . . . . . . . . . . 19 $/\$
61	8, 59, 60	syl2an 477	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
62	61	abscld 12914	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
63	61	absge0d 12922	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
64		elrege0 11384	. . . . . . . . . . . . . . . . 17 $/\$
65	62, 63, 64	sylanbrc 664	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
66		0e0icopnf 11387	. . . . . . . . . . . . . . . . 17
67	66	a1i 11	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
68	65, 67	ifclda 3816	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
69	68	ad2antrr 725	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
70		fconstmpt 4877	. . . . . . . . . . . . . . 15
71	70	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
72		eqidd 2439	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
73	55, 57, 69, 71, 72	offval2 6331	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
74		oveq2 6094	. . . . . . . . . . . . . . . 16
75		oveq2 6094	. . . . . . . . . . . . . . . 16
76	74, 75	ifsb 3797	. . . . . . . . . . . . . . 15
77	56	recnd 9404	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
78	77	adantr 465	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
79	78	mul01d 9560	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
80	79	ifeq2d 3803	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ $/\$
81	76, 80	syl5eq 2482	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
82	81	mpteq2dv 4374	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
83	73, 82	eqtrd 2470	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
84	83	fveq2d 5690	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
85	68	adantr 465	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
86		eqid 2438	. . . . . . . . . . . . . 14
87	85, 86	fmptd 5862	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
88	87	adantr 465	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
89		inss2 3566	. . . . . . . . . . . . . . . . . 18
90	89	a1i 11	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
91	23, 20	mbfdm2 21096	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
92	8	ffvelrnda 5838	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
93	8	feqmptd 5739	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
94		simplr 754	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
95	93, 94	eqeltrrd 2513	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
96	90, 91, 92, 95	iblss 21262	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
97	61, 96	iblabs 21286	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
98	62, 63	iblpos 21250	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ MblFn $/\$
99	97, 98	mpbid 210	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ MblFn $/\$
100	99	simprd 463	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
101	100	adantr 465	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
102		simplrl 759	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
103		neq0 3642	. . . . . . . . . . . . . . 15
104		0re 9378	. . . . . . . . . . . . . . . . . . 19
105	104	a1i 11	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
106	58	simplbi 460	. . . . . . . . . . . . . . . . . . . 20
107		ffvelrn 5836	. . . . . . . . . . . . . . . . . . . 20 $/\$
108	2, 106, 107	syl2an 477	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$ $/\$
109	108	abscld 12914	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
110		simplrl 759	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
111	108	absge0d 12922	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
112		simprr 756	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$
113		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . 22
114	113	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . 21
115	114	breq1d 4297	. . . . . . . . . . . . . . . . . . . 20
116	115	rspccva 3067	. . . . . . . . . . . . . . . . . . 19 $/\$
117	112, 106, 116	syl2an 477	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
118	105, 109, 110, 111, 117	letrd 9520	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
119	118	ex 434	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
120	119	exlimdv 1690	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
121	103, 120	syl5bi 217	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$
122	121	imp 429	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
123		elrege0 11384	. . . . . . . . . . . . 13 $/\$
124	102, 122, 123	sylanbrc 664	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
125	88, 101, 124	itg2mulc 21205	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
126	84, 125	eqtr3d 2472	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
127	102, 101	remulcld 9406	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
128	126, 127	eqeltrd 2512	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
129	128	ex 434	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
130		noel 3636	. . . . . . . . . . . . . 14
131		eleq2 2499	. . . . . . . . . . . . . 14
132	130, 131	mtbiri 303	. . . . . . . . . . . . 13
133		iffalse 3794	. . . . . . . . . . . . 13
134	132, 133	syl 16	. . . . . . . . . . . 12
135	134	mpteq2dv 4374	. . . . . . . . . . 11
136		fconstmpt 4877	. . . . . . . . . . 11
137	135, 136	syl6eqr 2488	. . . . . . . . . 10
138	137	fveq2d 5690	. . . . . . . . 9
139		itg20 21195	. . . . . . . . . 10
140	139, 104	eqeltri 2508	. . . . . . . . 9
141	138, 140	syl6eqel 2526	. . . . . . . 8
142	129, 141	pm2.61d2 160	. . . . . . 7 MblFn $/\$ $/\$ $/\$
143	110, 62	remulcld 9406	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
144	143	rexrd 9425	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
145	110, 62, 118, 63	mulge0d 9908	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
146		elxrge0 11386	. . . . . . . . . . . 12 $/\$
147	144, 145, 146	sylanbrc 664	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
148	147, 49	ifclda 3816	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
149	148	adantr 465	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
150		eqid 2438	. . . . . . . . 9
151	149, 150	fmptd 5862	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
152	108, 61	absmuld 12932	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
153		abscl 12759	. . . . . . . . . . . . . . . 16
154		absge0 12768	. . . . . . . . . . . . . . . 16
155	153, 154	jca 532	. . . . . . . . . . . . . . 15 $/\$
156	61, 155	syl 16	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
157		lemul1a 10175	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
158	109, 110, 156, 117, 157	syl31anc 1221	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
159	152, 158	eqbrtrd 4307	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
160		iftrue 3792	. . . . . . . . . . . . 13
161	160	adantl 466	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
162		iftrue 3792	. . . . . . . . . . . . 13
163	162	adantl 466	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
164	159, 161, 163	3brtr4d 4317	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
165		0le0 10403	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13
167		iffalse 3794	. . . . . . . . . . . . 13
168	166, 167, 133	3brtr4d 4317	. . . . . . . . . . . 12
169	168	adantl 466	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
170	164, 169	pm2.61dan 789	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
171	170	ralrimivw 2795	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
172	54	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
173		eqidd 2439	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
174		eqidd 2439	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
175	172, 51, 149, 173, 174	ofrfval2 6332	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
176	171, 175	mpbird 232	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
177		itg2le 21197	. . . . . . . 8 $/\$ $/\$
178	53, 151, 176, 177	syl3anc 1218	. . . . . . 7 MblFn $/\$ $/\$ $/\$
179		itg2lecl 21196	. . . . . . 7 $/\$ $/\$
180	53, 142, 178, 179	syl3anc 1218	. . . . . 6 MblFn $/\$ $/\$ $/\$
181	43, 45	iblpos 21250	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn $/\$
182	42, 180, 181	mpbir2and 913	. . . . 5 MblFn $/\$ $/\$ $/\$
183	20, 23, 182	iblabsr 21287	. . . 4 MblFn $/\$ $/\$ $/\$
184	18, 183	eqeltrd 2512	. . 3 MblFn $/\$ $/\$ $/\$
185	184	rexlimdvaa 2837	. 2 MblFn $/\$
186	185	3impia 1184	1 MblFn $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

wral 2710

wrex 2711

cvv 2967

cin 3322

wss 3323

c0 3632

cif 3786

csn 3872 class class class wbr 4287

cmpt 4345

cxp 4833

cdm 4835

ccom 4839

wfn 5408

wf 5409

cfv 5413 (class class class)co 6086

cof 6313

cofr 6314

cc 9272

cr 9273

cc0 9274

cmul 9279

cpnf 9407

cxr 9409

cle 9411

cico 11294

cicc 11295

cabs 12715

ccncf 20432

cvol 20927 MblFncmbf 21074

citg2 21076

cibl 21077

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cc 8596 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-disj 4258 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 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-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-ofr 6316 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-omul 6917 df-er 7093 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-acn 8104 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-hash 12096 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-sum 13156 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-submnd 15457 df-mulg 15539 df-cntz 15826 df-cmn 16270 df-psmet 17789 df-xmet 17790 df-met 17791 df-bl 17792 df-mopn 17793 df-cnfld 17799 df-top 18483 df-bases 18485 df-topon 18486 df-topsp 18487 df-cn 18811 df-cnp 18812 df-cmp 18970 df-tx 19115 df-hmeo 19308 df-xms 19875 df-ms 19876 df-tms 19877 df-cncf 20434 df-ovol 20928 df-vol 20929 df-mbf 21079 df-itg1 21080 df-itg2 21081 df-ibl 21082 df-0p 21128

This theorem is referenced by: bddibl 21297 itgsubstlem 21500

W3C validator