cnbdibl

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

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

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

Metamath Proof Explorer