cnioobibld

$( <MM> <PROOF_ASST> THEOREM=cnioobibld  LOC_AFTER=?

*
  A continuous function on an open interval which is bounded is integrable. See cniccibl for closed intervals.


h1::cnioobibld.1   |- ( ph -> A e. RR )
h2::cnioobibld.2   |- ( ph -> B e. RR )
h3::cnioobibld.3   |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
h4::cnioobibld.4   |- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )

10::ioombl         |- ( A (,) B ) e. dom vol
10a:10:a1i |- ( ph -> ( A (,) B ) e. dom vol )
20::cnmbf          |- ( ( ( A (,) B ) e. dom vol /\ F e. ( ( A (,) B ) -cn-> CC ) ) -> F e. MblFn )
20a:10a,3,20:syl2anc |- ( ph -> F e. MblFn )
*
30::cncff          |- ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
31::fdm            |- ( F : ( A (,) B ) --> CC -> dom F = ( A (,) B ) )
32:3,30,31:3syl |- ( ph -> dom F = ( A (,) B ) )
33:32:fveq2d       |- ( ph -> ( vol ` dom F ) = ( vol ` ( A (,) B ) ) )
34::ioovolcl       |- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )
35:1,2,34:syl2anc |- ( ph -> ( vol ` ( A (,) B ) ) e. RR )
36:33,35:eqeltrd |- ( ph -> ( vol ` dom F ) e. RR )
*
1000::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 )
qed:20a,36,4,1000:syl3anc |- ( ph -> F e. L^1 )

$=    ( cmbf wcel cdm cvol cfv cr cv co cc syl2anc cabs cle wral wrex
      wbr cibl cioo ccncf ioombl a1i cnmbf wceq cncff fdm 3syl fveq2d
      wf ioovolcl eqeltrd bddibl syl3anc ) AFKLZFMZNOZPLCQFOUAOBQUBUE
      CVCUCBPUDFUFLADEUGRZNMLZFVESUHRLZVBVFADEUIUJIVEFUKTAVDVENOZPAVC
      VENAVGVESFUQVCVEULIVESFUMVESFUNUOUPADPLEPLVHPLGHDEURTUSJBCFUTVA
      $.
$d x y
$d F x
$d F y
$)