Theorem cnbdibl

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

	Ref	Expression
Hypotheses	cnbdibl.a	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
	cnbdibl.va	⊢ ( 𝜑 → ( vol ‘ 𝐴 ) ∈ ℝ )
	cnbdibl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
	cnbdibl.bd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
Assertion	cnbdibl	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		cnbdibl.a	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
2		cnbdibl.va	⊢ ( 𝜑 → ( vol ‘ 𝐴 ) ∈ ℝ )
3		cnbdibl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
4		cnbdibl.bd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
5		cnmbf	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) → 𝐹 ∈ MblFn )
6	1 3 5	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
7		cncff	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
8		fdm	⊢ ( 𝐹 : 𝐴 ⟶ ℂ → dom 𝐹 = 𝐴 )
9	3 7 8	3syl	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
10	9	fveq2d	⊢ ( 𝜑 → ( vol ‘ dom 𝐹 ) = ( vol ‘ 𝐴 ) )
11	10 2	eqeltrd	⊢ ( 𝜑 → ( vol ‘ dom 𝐹 ) ∈ ℝ )
12		bddibl	⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )
13	6 11 4 12	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )