Metamath Proof Explorer

Theorem cniccibl

Description: A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion cniccibl 
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. L^1 )

Proof

Step Hyp Ref Expression
1 iccmbl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )
2 cnmbf 
 |-  ( ( ( A [,] B ) e. dom vol /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. MblFn )
3 1 2 stoic3 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. MblFn )
4 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. ( ( A [,] B ) -cn-> CC ) )
5 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
6 fdm 
 |-  ( F : ( A [,] B ) --> CC -> dom F = ( A [,] B ) )
7 4 5 6 3syl 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> dom F = ( A [,] B ) )
8 7 fveq2d 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( vol ` dom F ) = ( vol ` ( A [,] B ) ) )
9 iccvolcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,] B ) ) e. RR )
10 9 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( vol ` ( A [,] B ) ) e. RR )
11 8 10 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( vol ` dom F ) e. RR )
12 cniccbdd 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x )
13 7 raleqdv 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( A. y e. dom F ( abs ` ( F ` y ) ) <_ x <-> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) )
14 13 rexbidv 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x <-> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) )
15 12 14 mpbird 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
16 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 )
17 3 11 15 16 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. L^1 )