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

Theorem iblmbf 25802
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 25657 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
21ssrab3 4082 . 2 𝐿1 ⊆ MblFn
32sseli 3979 1 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wral 3061  csb 3899  ifcif 4525   class class class wbr 5143  cmpt 5225  dom cdm 5685  cfv 6561  (class class class)co 7431  cr 11154  0cc0 11155  ici 11157  cle 11296   / cdiv 11920  3c3 12322  ...cfz 13547  cexp 14102  cre 15136  MblFncmbf 25649  2citg2 25651  𝐿1cibl 25652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-ibl 25657
This theorem is referenced by:  iblcnlem  25824  itgcnlem  25825  itgcnval  25835  itgre  25836  itgim  25837  iblneg  25838  itgneg  25839  iblss  25840  iblss2  25841  itgge0  25846  itgss3  25850  itgless  25852  iblsub  25857  itgadd  25860  itgsub  25861  itgfsum  25862  iblabs  25864  iblmulc2  25866  itgmulc2  25869  itgabs  25870  itgsplit  25871  bddmulibl  25874  itggt0  25879  itgcn  25880  ditgswap  25894  ditgsplitlem  25895  ftc1a  26078  itgsubstlem  26089  iblulm  26450  itgulm  26451  ibladdnc  37684  itgaddnclem1  37685  itgaddnclem2  37686  itgaddnc  37687  iblsubnc  37688  itgsubnc  37689  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  itgmulc2nclem2  37694  itgmulc2nc  37695  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem2  37701  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem8  37707
  Copyright terms: Public domain W3C validator