This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnbdibl

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

Ref Expression
Hypotheses cnbdibl.a 
|- ( ph -> A e. dom vol )
cnbdibl.va 
|- ( ph -> ( vol ` A ) e. RR )
cnbdibl.f 
|- ( ph -> F e. ( A -cn-> CC ) )
cnbdibl.bd 
|- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
Assertion cnbdibl 
|- ( ph -> F e. L^1 )

Proof

Step Hyp Ref Expression
1 cnbdibl.a 
 |-  ( ph -> A e. dom vol )
2 cnbdibl.va 
 |-  ( ph -> ( vol ` A ) e. RR )
3 cnbdibl.f 
 |-  ( ph -> F e. ( A -cn-> CC ) )
4 cnbdibl.bd 
 |-  ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
5 cnmbf 
 |-  ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> F e. MblFn )
6 1 3 5 syl2anc 
 |-  ( ph -> F e. MblFn )
7 cncff 
 |-  ( F e. ( A -cn-> CC ) -> F : A --> CC )
8 fdm 
 |-  ( F : A --> CC -> dom F = A )
9 3 7 8 3syl 
 |-  ( ph -> dom F = A )
10 9 fveq2d 
 |-  ( ph -> ( vol ` dom F ) = ( vol ` A ) )
11 10 2 eqeltrd 
 |-  ( ph -> ( vol ` dom F ) e. RR )
12 bddibl 
 |-  ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F e. L^1 )
13 6 11 4 12 syl3anc 
 |-  ( ph -> F e. L^1 )