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

Theorem iblmbf 24362
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 24217 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
21ssrab3 4056 . 2 𝐿1 ⊆ MblFn
32sseli 3962 1 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2110  wral 3138  csb 3882  ifcif 4466   class class class wbr 5058  cmpt 5138  dom cdm 5549  cfv 6349  (class class class)co 7150  cr 10530  0cc0 10531  ici 10533  cle 10670   / cdiv 11291  3c3 11687  ...cfz 12886  cexp 13423  cre 14450  MblFncmbf 24209  2citg2 24211  𝐿1cibl 24212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3942  df-ss 3951  df-ibl 24217
This theorem is referenced by:  iblcnlem  24383  itgcnlem  24384  itgcnval  24394  itgre  24395  itgim  24396  iblneg  24397  itgneg  24398  iblss  24399  iblss2  24400  itgge0  24405  itgss3  24409  itgless  24411  iblsub  24416  itgadd  24419  itgsub  24420  itgfsum  24421  iblabs  24423  iblmulc2  24425  itgmulc2  24428  itgabs  24429  itgsplit  24430  bddmulibl  24433  itggt0  24436  itgcn  24437  ditgswap  24451  ditgsplitlem  24452  ftc1a  24628  itgsubstlem  24639  iblulm  24989  itgulm  24990  ibladdnc  34943  itgaddnclem1  34944  itgaddnclem2  34945  itgaddnc  34946  iblsubnc  34947  itgsubnc  34948  iblabsnclem  34949  iblabsnc  34950  iblmulc2nc  34951  itgmulc2nclem2  34953  itgmulc2nc  34954  itgabsnc  34955  ftc1cnnclem  34959  ftc1anclem2  34962  ftc1anclem4  34964  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem8  34968
  Copyright terms: Public domain W3C validator