bddmulibl - Metamath Proof Explorer

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

Theorem bddmulibl 21973

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 21762	. . . . . . 7 MblFn
2	1	ad2antrr 725	. . . . . 6 MblFn $/\$ $/\$ $/\$
3		ffn 5722	. . . . . 6
4	2, 3	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
5		iblmbf 21902	. . . . . . . 8 MblFn
6	5	ad2antlr 726	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
7		mbff 21762	. . . . . . 7 MblFn
8	6, 7	syl 16	. . . . . 6 MblFn $/\$ $/\$ $/\$
9		ffn 5722	. . . . . 6
10	8, 9	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
11		mbfdm 21763	. . . . . 6 MblFn
12	11	ad2antrr 725	. . . . 5 MblFn $/\$ $/\$ $/\$
13		mbfdm 21763	. . . . . 6 MblFn
14	6, 13	syl 16	. . . . 5 MblFn $/\$ $/\$ $/\$
15		eqid 2460	. . . . 5
16		eqidd 2461	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
17		eqidd 2461	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
18	4, 10, 12, 14, 15, 16, 17	offval 6522	. . . 4 MblFn $/\$ $/\$ $/\$
19		ovex 6300	. . . . . 6
20	19	a1i 11	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
21		simpll 753	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
22	21, 6	mbfmul 21861	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
23	18, 22	eqeltrrd 2549	. . . . 5 MblFn $/\$ $/\$ $/\$ MblFn
24	23, 20	mbfmptcl 21772	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
25		eqidd 2461	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
26		absf 13119	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
28	27	feqmptd 5911	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
29		fveq2 5857	. . . . . . . 8
30	24, 25, 28, 29	fmptco 6045	. . . . . . 7 MblFn $/\$ $/\$ $/\$
31		eqid 2460	. . . . . . . . 9
32	24, 31	fmptd 6036	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
33		ax-resscn 9538	. . . . . . . . . . 11
34		ssid 3516	. . . . . . . . . . 11
35		cncfss 21131	. . . . . . . . . . 11 $/\$
36	33, 34, 35	mp2an 672	. . . . . . . . . 10
37		abscncf 21133	. . . . . . . . . 10
38	36, 37	sselii 3494	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
40		cncombf 21793	. . . . . . . 8 MblFn $/\$ $/\$ MblFn
41	23, 32, 39, 40	syl3anc 1223	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
42	30, 41	eqeltrrd 2549	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
43	24	abscld 13216	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
44	43	rexrd 9632	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
45	24	absge0d 13224	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
46		elxrge0 11618	. . . . . . . . . . 11 $/\$
47	44, 45, 46	sylanbrc 664	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
48		0e0iccpnf 11620	. . . . . . . . . . 11
49	48	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
50	47, 49	ifclda 3964	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
51	50	adantr 465	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
52		eqid 2460	. . . . . . . 8
53	51, 52	fmptd 6036	. . . . . . 7 MblFn $/\$ $/\$ $/\$
54		reex 9572	. . . . . . . . . . . . . . 15
55	54	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
56		simprl 755	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
57	56	ad2antrr 725	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
58		elin 3680	. . . . . . . . . . . . . . . . . . . 20 $/\$
59	58	simprbi 464	. . . . . . . . . . . . . . . . . . 19
60		ffvelrn 6010	. . . . . . . . . . . . . . . . . . 19 $/\$
61	8, 59, 60	syl2an 477	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
62	61	abscld 13216	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
63	61	absge0d 13224	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
64		elrege0 11616	. . . . . . . . . . . . . . . . 17 $/\$
65	62, 63, 64	sylanbrc 664	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
66		0e0icopnf 11619	. . . . . . . . . . . . . . . . 17
67	66	a1i 11	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
68	65, 67	ifclda 3964	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
69	68	ad2antrr 725	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
70		fconstmpt 5035	. . . . . . . . . . . . . . 15
71	70	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
72		eqidd 2461	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
73	55, 57, 69, 71, 72	offval2 6531	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
74		oveq2 6283	. . . . . . . . . . . . . . . 16
75		oveq2 6283	. . . . . . . . . . . . . . . 16
76	74, 75	ifsb 3945	. . . . . . . . . . . . . . 15
77	56	recnd 9611	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
78	77	adantr 465	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
79	78	mul01d 9767	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
80	79	ifeq2d 3951	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ $/\$
81	76, 80	syl5eq 2513	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
82	81	mpteq2dv 4527	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
83	73, 82	eqtrd 2501	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
84	83	fveq2d 5861	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
85	68	adantr 465	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
86		eqid 2460	. . . . . . . . . . . . . 14
87	85, 86	fmptd 6036	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
88	87	adantr 465	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
89		inss2 3712	. . . . . . . . . . . . . . . . . 18
90	89	a1i 11	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
91	23, 20	mbfdm2 21773	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
92	8	ffvelrnda 6012	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
93	8	feqmptd 5911	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
94		simplr 754	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
95	93, 94	eqeltrrd 2549	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
96	90, 91, 92, 95	iblss 21939	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
97	61, 96	iblabs 21963	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
98	62, 63	iblpos 21927	. . . . . . . . . . . . . . 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 3788	. . . . . . . . . . . . . . 15
104		0re 9585	. . . . . . . . . . . . . . . . . . 19
105	104	a1i 11	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
106	58	simplbi 460	. . . . . . . . . . . . . . . . . . . 20
107		ffvelrn 6010	. . . . . . . . . . . . . . . . . . . 20 $/\$
108	2, 106, 107	syl2an 477	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$ $/\$
109	108	abscld 13216	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
110		simplrl 759	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
111	108	absge0d 13224	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
112		simprr 756	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$
113		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . 22
114	113	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . 21
115	114	breq1d 4450	. . . . . . . . . . . . . . . . . . . 20
116	115	rspccva 3206	. . . . . . . . . . . . . . . . . . 19 $/\$
117	112, 106, 116	syl2an 477	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
118	105, 109, 110, 111, 117	letrd 9727	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
119	118	ex 434	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
120	119	exlimdv 1695	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
121	103, 120	syl5bi 217	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$
122	121	imp 429	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
123		elrege0 11616	. . . . . . . . . . . . 13 $/\$
124	102, 122, 123	sylanbrc 664	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
125	88, 101, 124	itg2mulc 21882	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
126	84, 125	eqtr3d 2503	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
127	102, 101	remulcld 9613	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
128	126, 127	eqeltrd 2548	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
129	128	ex 434	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
130		noel 3782	. . . . . . . . . . . . . 14
131		eleq2 2533	. . . . . . . . . . . . . 14
132	130, 131	mtbiri 303	. . . . . . . . . . . . 13
133		iffalse 3941	. . . . . . . . . . . . 13
134	132, 133	syl 16	. . . . . . . . . . . 12
135	134	mpteq2dv 4527	. . . . . . . . . . 11
136		fconstmpt 5035	. . . . . . . . . . 11
137	135, 136	syl6eqr 2519	. . . . . . . . . 10
138	137	fveq2d 5861	. . . . . . . . 9
139		itg20 21872	. . . . . . . . . 10
140	139, 104	eqeltri 2544	. . . . . . . . 9
141	138, 140	syl6eqel 2556	. . . . . . . 8
142	129, 141	pm2.61d2 160	. . . . . . 7 MblFn $/\$ $/\$ $/\$
143	110, 62	remulcld 9613	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
144	143	rexrd 9632	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
145	110, 62, 118, 63	mulge0d 10118	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
146		elxrge0 11618	. . . . . . . . . . . 12 $/\$
147	144, 145, 146	sylanbrc 664	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
148	147, 49	ifclda 3964	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
149	148	adantr 465	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
150		eqid 2460	. . . . . . . . 9
151	149, 150	fmptd 6036	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
152	108, 61	absmuld 13234	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
153		abscl 13061	. . . . . . . . . . . . . . . 16
154		absge0 13070	. . . . . . . . . . . . . . . 16
155	153, 154	jca 532	. . . . . . . . . . . . . . 15 $/\$
156	61, 155	syl 16	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
157		lemul1a 10385	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
158	109, 110, 156, 117, 157	syl31anc 1226	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
159	152, 158	eqbrtrd 4460	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
160		iftrue 3938	. . . . . . . . . . . . 13
161	160	adantl 466	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
162		iftrue 3938	. . . . . . . . . . . . 13
163	162	adantl 466	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
164	159, 161, 163	3brtr4d 4470	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
165		0le0 10614	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13
167		iffalse 3941	. . . . . . . . . . . . 13
168	166, 167, 133	3brtr4d 4470	. . . . . . . . . . . 12
169	168	adantl 466	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
170	164, 169	pm2.61dan 789	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
171	170	ralrimivw 2872	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
172	54	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
173		eqidd 2461	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
174		eqidd 2461	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
175	172, 51, 149, 173, 174	ofrfval2 6532	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
176	171, 175	mpbird 232	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
177		itg2le 21874	. . . . . . . 8 $/\$ $/\$
178	53, 151, 176, 177	syl3anc 1223	. . . . . . 7 MblFn $/\$ $/\$ $/\$
179		itg2lecl 21873	. . . . . . 7 $/\$ $/\$
180	53, 142, 178, 179	syl3anc 1223	. . . . . 6 MblFn $/\$ $/\$ $/\$
181	43, 45	iblpos 21927	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn $/\$
182	42, 180, 181	mpbir2and 915	. . . . 5 MblFn $/\$ $/\$ $/\$
183	20, 23, 182	iblabsr 21964	. . . 4 MblFn $/\$ $/\$ $/\$
184	18, 183	eqeltrd 2548	. . 3 MblFn $/\$ $/\$ $/\$
185	184	rexlimdvaa 2949	. 2 MblFn $/\$
186	185	3impia 1188	1 MblFn $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1374

wex 1591

wcel 1762

wral 2807

wrex 2808

cvv 3106

cin 3468

wss 3469

c0 3778

cif 3932

csn 4020 class class class wbr 4440

cmpt 4498

cxp 4990

cdm 4992

ccom 4996

wfn 5574

wf 5575

cfv 5579 (class class class)co 6275

cof 6513

cofr 6514

cc 9479

cr 9480

cc0 9481

cmul 9486

cpnf 9614

cxr 9616

cle 9618

cico 11520

cicc 11521

cabs 13017

ccncf 21108

cvol 21603 MblFncmbf 21751

citg2 21753

cibl 21754

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-inf2 8047 ax-cc 8804 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559 ax-addf 9560 ax-mulf 9561

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-fal 1380 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-iin 4321 df-disj 4411 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-of 6515 df-ofr 6516 df-om 6672 df-1st 6774 df-2nd 6775 df-supp 6892 df-recs 7032 df-rdg 7066 df-1o 7120 df-2o 7121 df-oadd 7124 df-omul 7125 df-er 7301 df-map 7412 df-pm 7413 df-ixp 7460 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-fsupp 7819 df-fi 7860 df-sup 7890 df-oi 7924 df-card 8309 df-acn 8312 df-cda 8537 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-div 10196 df-nn 10526 df-2 10583 df-3 10584 df-4 10585 df-5 10586 df-6 10587 df-7 10588 df-8 10589 df-9 10590 df-10 10591 df-n0 10785 df-z 10854 df-dec 10966 df-uz 11072 df-q 11172 df-rp 11210 df-xneg 11307 df-xadd 11308 df-xmul 11309 df-ioo 11522 df-ioc 11523 df-ico 11524 df-icc 11525 df-fz 11662 df-fzo 11782 df-fl 11886 df-mod 11953 df-seq 12064 df-exp 12123 df-hash 12361 df-cj 12882 df-re 12883 df-im 12884 df-sqr 13018 df-abs 13019 df-limsup 13243 df-clim 13260 df-rlim 13261 df-sum 13458 df-struct 14481 df-ndx 14482 df-slot 14483 df-base 14484 df-sets 14485 df-ress 14486 df-plusg 14557 df-mulr 14558 df-starv 14559 df-sca 14560 df-vsca 14561 df-ip 14562 df-tset 14563 df-ple 14564 df-ds 14566 df-unif 14567 df-hom 14568 df-cco 14569 df-rest 14667 df-topn 14668 df-0g 14686 df-gsum 14687 df-topgen 14688 df-pt 14689 df-prds 14692 df-xrs 14746 df-qtop 14751 df-imas 14752 df-xps 14754 df-mre 14830 df-mrc 14831 df-acs 14833 df-mnd 15721 df-submnd 15771 df-mulg 15854 df-cntz 16143 df-cmn 16589 df-psmet 18175 df-xmet 18176 df-met 18177 df-bl 18178 df-mopn 18179 df-cnfld 18185 df-top 19159 df-bases 19161 df-topon 19162 df-topsp 19163 df-cn 19487 df-cnp 19488 df-cmp 19646 df-tx 19791 df-hmeo 19984 df-xms 20551 df-ms 20552 df-tms 20553 df-cncf 21110 df-ovol 21604 df-vol 21605 df-mbf 21756 df-itg1 21757 df-itg2 21758 df-ibl 21759 df-0p 21805

This theorem is referenced by: bddibl 21974 itgsubstlem 22177 fourierdlem16 31242 fourierdlem21 31247 fourierdlem22 31248 fourierdlem83 31309

W3C validator