bddmulibl - Metamath Proof Explorer

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

Theorem bddmulibl 22875

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 22662	. . . . . . 7 MblFn
2	1	ad2antrr 740	. . . . . 6 MblFn $/\$ $/\$ $/\$
3		ffn 5739	. . . . . 6
4	2, 3	syl 17	. . . . 5 MblFn $/\$ $/\$ $/\$
5		iblmbf 22804	. . . . . . . 8 MblFn
6	5	ad2antlr 741	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
7		mbff 22662	. . . . . . 7 MblFn
8	6, 7	syl 17	. . . . . 6 MblFn $/\$ $/\$ $/\$
9		ffn 5739	. . . . . 6
10	8, 9	syl 17	. . . . 5 MblFn $/\$ $/\$ $/\$
11		mbfdm 22663	. . . . . 6 MblFn
12	11	ad2antrr 740	. . . . 5 MblFn $/\$ $/\$ $/\$
13		mbfdm 22663	. . . . . 6 MblFn
14	6, 13	syl 17	. . . . 5 MblFn $/\$ $/\$ $/\$
15		eqid 2471	. . . . 5
16		eqidd 2472	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
17		eqidd 2472	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
18	4, 10, 12, 14, 15, 16, 17	offval 6557	. . . 4 MblFn $/\$ $/\$ $/\$
19		ovex 6336	. . . . . 6
20	19	a1i 11	. . . . 5 MblFn $/\$ $/\$ $/\$ $/\$
21		simpll 768	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
22	21, 6	mbfmul 22763	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
23	18, 22	eqeltrrd 2550	. . . . 5 MblFn $/\$ $/\$ $/\$ MblFn
24	23, 20	mbfmptcl 22672	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
25		eqidd 2472	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
26		absf 13477	. . . . . . . . . 10
27	26	a1i 11	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
28	27	feqmptd 5932	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
29		fveq2 5879	. . . . . . . 8
30	24, 25, 28, 29	fmptco 6072	. . . . . . 7 MblFn $/\$ $/\$ $/\$
31		eqid 2471	. . . . . . . . 9
32	24, 31	fmptd 6061	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
33		ax-resscn 9614	. . . . . . . . . . 11
34		ssid 3437	. . . . . . . . . . 11
35		cncfss 22009	. . . . . . . . . . 11 $/\$
36	33, 34, 35	mp2an 686	. . . . . . . . . 10
37		abscncf 22011	. . . . . . . . . 10
38	36, 37	sselii 3415	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
40		cncombf 22693	. . . . . . . 8 MblFn $/\$ $/\$ MblFn
41	23, 32, 39, 40	syl3anc 1292	. . . . . . 7 MblFn $/\$ $/\$ $/\$ MblFn
42	30, 41	eqeltrrd 2550	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn
43	24	abscld 13575	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
44	43	rexrd 9708	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
45	24	absge0d 13583	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
46		elxrge0 11767	. . . . . . . . . . 11 $/\$
47	44, 45, 46	sylanbrc 677	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
48		0e0iccpnf 11769	. . . . . . . . . . 11
49	48	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
50	47, 49	ifclda 3904	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
51	50	adantr 472	. . . . . . . 8 MblFn $/\$ $/\$ $/\$ $/\$
52		eqid 2471	. . . . . . . 8
53	51, 52	fmptd 6061	. . . . . . 7 MblFn $/\$ $/\$ $/\$
54		reex 9648	. . . . . . . . . . . . . . 15
55	54	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
56		simprl 772	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
57	56	ad2antrr 740	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
58		elin 3608	. . . . . . . . . . . . . . . . . . . 20 $/\$
59	58	simprbi 471	. . . . . . . . . . . . . . . . . . 19
60		ffvelrn 6035	. . . . . . . . . . . . . . . . . . 19 $/\$
61	8, 59, 60	syl2an 485	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
62	61	abscld 13575	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
63	61	absge0d 13583	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
64		elrege0 11764	. . . . . . . . . . . . . . . . 17 $/\$
65	62, 63, 64	sylanbrc 677	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
66		0e0icopnf 11768	. . . . . . . . . . . . . . . . 17
67	66	a1i 11	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
68	65, 67	ifclda 3904	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
69	68	ad2antrr 740	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
70		fconstmpt 4883	. . . . . . . . . . . . . . 15
71	70	a1i 11	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
72		eqidd 2472	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
73	55, 57, 69, 71, 72	offval2 6567	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
74		ovif2 6393	. . . . . . . . . . . . . . 15
75	56	recnd 9687	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
76	75	adantr 472	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
77	76	mul01d 9850	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$ $/\$
78	77	ifeq2d 3891	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ $/\$
79	74, 78	syl5eq 2517	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
80	79	mpteq2dv 4483	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
81	73, 80	eqtrd 2505	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
82	81	fveq2d 5883	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
83	68	adantr 472	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$
84		eqid 2471	. . . . . . . . . . . . . 14
85	83, 84	fmptd 6061	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
86	85	adantr 472	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
87		inss2 3644	. . . . . . . . . . . . . . . . . 18
88	87	a1i 11	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
89	23, 20	mbfdm2 22673	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
90	8	ffvelrnda 6037	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
91	8	feqmptd 5932	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
92		simplr 770	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$
93	91, 92	eqeltrrd 2550	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$
94	88, 89, 90, 93	iblss 22841	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
95	61, 94	iblabs 22865	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
96	62, 63	iblpos 22829	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$ MblFn $/\$
97	95, 96	mpbid 215	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ MblFn $/\$
98	97	simprd 470	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$
99	98	adantr 472	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
100		simplrl 778	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
101		neq0 3733	. . . . . . . . . . . . . . 15
102		0re 9661	. . . . . . . . . . . . . . . . . . 19
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
104	58	simplbi 467	. . . . . . . . . . . . . . . . . . . 20
105		ffvelrn 6035	. . . . . . . . . . . . . . . . . . . 20 $/\$
106	2, 104, 105	syl2an 485	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$ $/\$
107	106	abscld 13575	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
108		simplrl 778	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
109	106	absge0d 13583	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
110		simprr 774	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ $/\$ $/\$
111		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22
112	111	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
113	112	breq1d 4405	. . . . . . . . . . . . . . . . . . . 20
114	113	rspccva 3135	. . . . . . . . . . . . . . . . . . 19 $/\$
115	110, 104, 114	syl2an 485	. . . . . . . . . . . . . . . . . 18 MblFn $/\$ $/\$ $/\$ $/\$
116	103, 107, 108, 109, 115	letrd 9809	. . . . . . . . . . . . . . . . 17 MblFn $/\$ $/\$ $/\$ $/\$
117	116	ex 441	. . . . . . . . . . . . . . . 16 MblFn $/\$ $/\$ $/\$
118	117	exlimdv 1787	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$ $/\$
119	101, 118	syl5bi 225	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$
120	119	imp 436	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
121		elrege0 11764	. . . . . . . . . . . . 13 $/\$
122	100, 120, 121	sylanbrc 677	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
123	86, 99, 122	itg2mulc 22784	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
124	82, 123	eqtr3d 2507	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
125	100, 99	remulcld 9689	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$ $/\$
126	124, 125	eqeltrd 2549	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
127	126	ex 441	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
128		noel 3726	. . . . . . . . . . . . . 14
129		eleq2 2538	. . . . . . . . . . . . . 14
130	128, 129	mtbiri 310	. . . . . . . . . . . . 13
131		iffalse 3881	. . . . . . . . . . . . 13
132	130, 131	syl 17	. . . . . . . . . . . 12
133	132	mpteq2dv 4483	. . . . . . . . . . 11
134		fconstmpt 4883	. . . . . . . . . . 11
135	133, 134	syl6eqr 2523	. . . . . . . . . 10
136	135	fveq2d 5883	. . . . . . . . 9
137		itg20 22774	. . . . . . . . . 10
138	137, 102	eqeltri 2545	. . . . . . . . 9
139	136, 138	syl6eqel 2557	. . . . . . . 8
140	127, 139	pm2.61d2 165	. . . . . . 7 MblFn $/\$ $/\$ $/\$
141	108, 62	remulcld 9689	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
142	141	rexrd 9708	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
143	108, 62, 116, 63	mulge0d 10211	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
144		elxrge0 11767	. . . . . . . . . . . 12 $/\$
145	142, 143, 144	sylanbrc 677	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
146	145, 49	ifclda 3904	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
147	146	adantr 472	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$ $/\$
148		eqid 2471	. . . . . . . . 9
149	147, 148	fmptd 6061	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
150	106, 61	absmuld 13593	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
151		abscl 13418	. . . . . . . . . . . . . . . 16
152		absge0 13427	. . . . . . . . . . . . . . . 16
153	151, 152	jca 541	. . . . . . . . . . . . . . 15 $/\$
154	61, 153	syl 17	. . . . . . . . . . . . . 14 MblFn $/\$ $/\$ $/\$ $/\$ $/\$
155		lemul1a 10481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
156	107, 108, 154, 115, 155	syl31anc 1295	. . . . . . . . . . . . 13 MblFn $/\$ $/\$ $/\$ $/\$
157	150, 156	eqbrtrd 4416	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
158		iftrue 3878	. . . . . . . . . . . . 13
159	158	adantl 473	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
160		iftrue 3878	. . . . . . . . . . . . 13
161	160	adantl 473	. . . . . . . . . . . 12 MblFn $/\$ $/\$ $/\$ $/\$
162	157, 159, 161	3brtr4d 4426	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
163		0le0 10721	. . . . . . . . . . . . . 14
164	163	a1i 11	. . . . . . . . . . . . 13
165		iffalse 3881	. . . . . . . . . . . . 13
166	164, 165, 131	3brtr4d 4426	. . . . . . . . . . . 12
167	166	adantl 473	. . . . . . . . . . 11 MblFn $/\$ $/\$ $/\$ $/\$
168	162, 167	pm2.61dan 808	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
169	168	ralrimivw 2810	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
170	54	a1i 11	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
171		eqidd 2472	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
172		eqidd 2472	. . . . . . . . . 10 MblFn $/\$ $/\$ $/\$
173	170, 51, 147, 171, 172	ofrfval2 6568	. . . . . . . . 9 MblFn $/\$ $/\$ $/\$
174	169, 173	mpbird 240	. . . . . . . 8 MblFn $/\$ $/\$ $/\$
175		itg2le 22776	. . . . . . . 8 $/\$ $/\$
176	53, 149, 174, 175	syl3anc 1292	. . . . . . 7 MblFn $/\$ $/\$ $/\$
177		itg2lecl 22775	. . . . . . 7 $/\$ $/\$
178	53, 140, 176, 177	syl3anc 1292	. . . . . 6 MblFn $/\$ $/\$ $/\$
179	43, 45	iblpos 22829	. . . . . 6 MblFn $/\$ $/\$ $/\$ MblFn $/\$
180	42, 178, 179	mpbir2and 936	. . . . 5 MblFn $/\$ $/\$ $/\$
181	20, 23, 180	iblabsr 22866	. . . 4 MblFn $/\$ $/\$ $/\$
182	18, 181	eqeltrd 2549	. . 3 MblFn $/\$ $/\$ $/\$
183	182	rexlimdvaa 2872	. 2 MblFn $/\$
184	183	3impia 1228	1 MblFn $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

wral 2756

wrex 2757

cvv 3031

cin 3389

wss 3390

c0 3722

cif 3872

csn 3959 class class class wbr 4395

cmpt 4454

cxp 4837

cdm 4839

ccom 4843

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cof 6548

cofr 6549

cc 9555

cr 9556

cc0 9557

cmul 9562

cpnf 9690

cxr 9692

cle 9694

cico 11662

cicc 11663

cabs 13374

ccncf 21986

cvol 22493 MblFncmbf 22651

citg2 22653

cibl 22654

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-cc 8883 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-ofr 6551 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-omul 7205 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-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-hash 12554 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-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-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cn 20320 df-cnp 20321 df-cmp 20479 df-tx 20654 df-hmeo 20847 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-ovol 22494 df-vol 22496 df-mbf 22656 df-itg1 22657 df-itg2 22658 df-ibl 22659 df-0p 22707

This theorem is referenced by: bddibl 22876 itgsubstlem 23079 fourierdlem16 38097 fourierdlem21 38102 fourierdlem22 38103 fourierdlem83 38165

W3C validator