Theorem cnioobibld

Description: A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider F = ( x e. ( 0 (,) 1 ) |-> ( 1 / x ) ) . See cniccibl for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019)

	Ref	Expression
Hypotheses	cnioobibld.1	|- ( ph -> A e. RR )
	cnioobibld.2	|- ( ph -> B e. RR )
	cnioobibld.3	|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
	cnioobibld.4	|- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
Assertion	cnioobibld	|- ( ph -> F e. L^1 )

Proof

Step	Hyp	Ref	Expression
1		cnioobibld.1	|- ( ph -> A e. RR )
2		cnioobibld.2	|- ( ph -> B e. RR )
3		cnioobibld.3	|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
4		cnioobibld.4	|- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )
5		ioombl	|- ( A (,) B ) e. dom vol
6		cnmbf	|- ( ( ( A (,) B ) e. dom vol /\ F e. ( ( A (,) B ) -cn-> CC ) ) -> F e. MblFn )
7	5 3 6	sylancr	|- ( ph -> F e. MblFn )
8		cncff	|- ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
9		fdm	|- ( F : ( A (,) B ) --> CC -> dom F = ( A (,) B ) )
10	3 8 9	3syl	|- ( ph -> dom F = ( A (,) B ) )
11	10	fveq2d	|- ( ph -> ( vol ` dom F ) = ( vol ` ( A (,) B ) ) )
12		ioovolcl	|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )
13	1 2 12	syl2anc	|- ( ph -> ( vol ` ( A (,) B ) ) e. RR )
14	11 13	eqeltrd	|- ( ph -> ( vol ` dom F ) e. RR )
15		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 )
16	7 14 4 15	syl3anc	|- ( ph -> F e. L^1 )