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

Theorem iblmbf 23733
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 23590 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2 ssrab2 3828 . . 3 {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ} ⊆ MblFn
31, 2eqsstri 3776 . 2 𝐿1 ⊆ MblFn
43sseli 3740 1 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139  wral 3050  {crab 3054  csb 3674  ifcif 4230   class class class wbr 4804  cmpt 4881  dom cdm 5266  cfv 6049  (class class class)co 6813  cr 10127  0cc0 10128  ici 10130  cle 10267   / cdiv 10876  3c3 11263  ...cfz 12519  cexp 13054  cre 14036  MblFncmbf 23582  2citg2 23584  𝐿1cibl 23585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-in 3722  df-ss 3729  df-ibl 23590
This theorem is referenced by:  iblcnlem  23754  itgcnlem  23755  itgcnval  23765  itgre  23766  itgim  23767  iblneg  23768  itgneg  23769  iblss  23770  iblss2  23771  itgge0  23776  itgss3  23780  itgless  23782  iblsub  23787  itgadd  23790  itgsub  23791  itgfsum  23792  iblabs  23794  iblmulc2  23796  itgmulc2  23799  itgabs  23800  itgsplit  23801  bddmulibl  23804  itggt0  23807  itgcn  23808  ditgswap  23822  ditgsplitlem  23823  ftc1a  23999  itgsubstlem  24010  iblulm  24360  itgulm  24361  ibladdnc  33780  itgaddnclem1  33781  itgaddnclem2  33782  itgaddnc  33783  iblsubnc  33784  itgsubnc  33785  iblabsnclem  33786  iblabsnc  33787  iblmulc2nc  33788  itgmulc2nclem2  33790  itgmulc2nc  33791  itgabsnc  33792  ftc1cnnclem  33796  ftc1anclem2  33799  ftc1anclem4  33801  ftc1anclem5  33802  ftc1anclem6  33803  ftc1anclem8  33805
  Copyright terms: Public domain W3C validator