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

Theorem iblmbf 23824
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 23679 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2 ssrab2 3846 . . 3 {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ} ⊆ MblFn
31, 2eqsstri 3794 . 2 𝐿1 ⊆ MblFn
43sseli 3756 1 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2155  wral 3054  {crab 3058  csb 3690  ifcif 4242   class class class wbr 4808  cmpt 4887  dom cdm 5276  cfv 6067  (class class class)co 6841  cr 10187  0cc0 10188  ici 10190  cle 10328   / cdiv 10937  3c3 11327  ...cfz 12532  cexp 13066  cre 14123  MblFncmbf 23671  2citg2 23673  𝐿1cibl 23674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-rab 3063  df-in 3738  df-ss 3745  df-ibl 23679
This theorem is referenced by:  iblcnlem  23845  itgcnlem  23846  itgcnval  23856  itgre  23857  itgim  23858  iblneg  23859  itgneg  23860  iblss  23861  iblss2  23862  itgge0  23867  itgss3  23871  itgless  23873  iblsub  23878  itgadd  23881  itgsub  23882  itgfsum  23883  iblabs  23885  iblmulc2  23887  itgmulc2  23890  itgabs  23891  itgsplit  23892  bddmulibl  23895  itggt0  23898  itgcn  23899  ditgswap  23913  ditgsplitlem  23914  ftc1a  24090  itgsubstlem  24101  iblulm  24451  itgulm  24452  ibladdnc  33822  itgaddnclem1  33823  itgaddnclem2  33824  itgaddnc  33825  iblsubnc  33826  itgsubnc  33827  iblabsnclem  33828  iblabsnc  33829  iblmulc2nc  33830  itgmulc2nclem2  33832  itgmulc2nc  33833  itgabsnc  33834  ftc1cnnclem  33838  ftc1anclem2  33841  ftc1anclem4  33843  ftc1anclem5  33844  ftc1anclem6  33845  ftc1anclem8  33847
  Copyright terms: Public domain W3C validator