Theorem cnbdibl

Description: A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cnbdibl.a	$$⊢\phi \to A\in \mathrm{dom}vol$$
	cnbdibl.va	$$⊢\phi \to vol\left(A\right)\in ℝ$$
	cnbdibl.f	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
	cnbdibl.bd	$$⊢\phi \to \exists x\in ℝ\forall y\in \mathrm{dom}F\left|F\left(y\right)\right|\le x$$
Assertion	cnbdibl	$$⊢\phi \to F\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		cnbdibl.a	$$⊢\phi \to A\in \mathrm{dom}vol$$
2		cnbdibl.va	$$⊢\phi \to vol\left(A\right)\in ℝ$$
3		cnbdibl.f	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
4		cnbdibl.bd	$$⊢\phi \to \exists x\in ℝ\forall y\in \mathrm{dom}F\left|F\left(y\right)\right|\le x$$
5		cnmbf	$$⊢\left(A\in \mathrm{dom}vol\wedge F:A\underset{cn}{⟶}ℂ\right)\to F\in MblFn$$
6	1 3 5	syl2anc	$$⊢\phi \to F\in MblFn$$
7		cncff	$$⊢F:A\underset{cn}{⟶}ℂ\to F:A⟶ℂ$$
8		fdm	$$⊢F:A⟶ℂ\to \mathrm{dom}F=A$$
9	3 7 8	3syl	$$⊢\phi \to \mathrm{dom}F=A$$
10	9	fveq2d	$$⊢\phi \to vol\left(\mathrm{dom}F\right)=vol\left(A\right)$$
11	10 2	eqeltrd	$$⊢\phi \to vol\left(\mathrm{dom}F\right)\in ℝ$$
12		bddibl	$$⊢\left(F\in MblFn\wedge vol\left(\mathrm{dom}F\right)\in ℝ\wedge \exists x\in ℝ\forall y\in \mathrm{dom}F\left|F\left(y\right)\right|\le x\right)\to F\in {𝐿}^1$$
13	6 11 4 12	syl3anc	$$⊢\phi \to F\in {𝐿}^1$$