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 )