MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iblmbf Structured version   Visualization version   GIF version

Theorem iblmbf 25741
Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
Assertion
Ref Expression
iblmbf (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)

Proof of Theorem iblmbf
Dummy variables 𝑓 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ibl 25595 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
21ssrab3 4076 . 2 𝐿1 ⊆ MblFn
32sseli 3972 1 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2098  wral 3050  csb 3889  ifcif 4530   class class class wbr 5149  cmpt 5232  dom cdm 5678  cfv 6549  (class class class)co 7419  cr 11139  0cc0 11140  ici 11142  cle 11281   / cdiv 11903  3c3 12301  ...cfz 13519  cexp 14062  cre 15080  MblFncmbf 25587  2citg2 25589  𝐿1cibl 25590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-ss 3961  df-ibl 25595
This theorem is referenced by:  iblcnlem  25762  itgcnlem  25763  itgcnval  25773  itgre  25774  itgim  25775  iblneg  25776  itgneg  25777  iblss  25778  iblss2  25779  itgge0  25784  itgss3  25788  itgless  25790  iblsub  25795  itgadd  25798  itgsub  25799  itgfsum  25800  iblabs  25802  iblmulc2  25804  itgmulc2  25807  itgabs  25808  itgsplit  25809  bddmulibl  25812  itggt0  25817  itgcn  25818  ditgswap  25832  ditgsplitlem  25833  ftc1a  26016  itgsubstlem  26027  iblulm  26388  itgulm  26389  ibladdnc  37281  itgaddnclem1  37282  itgaddnclem2  37283  itgaddnc  37284  iblsubnc  37285  itgsubnc  37286  iblabsnclem  37287  iblabsnc  37288  iblmulc2nc  37289  itgmulc2nclem2  37291  itgmulc2nc  37292  itgabsnc  37293  ftc1cnnclem  37295  ftc1anclem2  37298  ftc1anclem4  37300  ftc1anclem5  37301  ftc1anclem6  37302  ftc1anclem8  37304
  Copyright terms: Public domain W3C validator