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

Theorem iblmbf 23257
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 23114 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2 ssrab2 3649 . . 3 {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ} ⊆ MblFn
31, 2eqsstri 3597 . 2 𝐿1 ⊆ MblFn
43sseli 3563 1 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wral 2895  {crab 2899  csb 3498  ifcif 4035   class class class wbr 4577  cmpt 4637  dom cdm 5028  cfv 5790  (class class class)co 6527  cr 9791  0cc0 9792  ici 9794  cle 9931   / cdiv 10533  3c3 10918  ...cfz 12152  cexp 12677  cre 13631  MblFncmbf 23106  2citg2 23108  𝐿1cibl 23109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-in 3546  df-ss 3553  df-ibl 23114
This theorem is referenced by:  iblcnlem  23278  itgcnlem  23279  itgcnval  23289  itgre  23290  itgim  23291  iblneg  23292  itgneg  23293  iblss  23294  iblss2  23295  itgge0  23300  itgss3  23304  itgless  23306  iblsub  23311  itgadd  23314  itgsub  23315  itgfsum  23316  iblabs  23318  iblmulc2  23320  itgmulc2  23323  itgabs  23324  itgsplit  23325  bddmulibl  23328  itggt0  23331  itgcn  23332  ditgswap  23346  ditgsplitlem  23347  ftc1a  23521  itgsubstlem  23532  iblulm  23882  itgulm  23883  ibladdnc  32440  itgaddnclem1  32441  itgaddnclem2  32442  itgaddnc  32443  iblsubnc  32444  itgsubnc  32445  iblabsnclem  32446  iblabsnc  32447  iblmulc2nc  32448  itgmulc2nclem2  32450  itgmulc2nc  32451  itgabsnc  32452  ftc1cnnclem  32456  ftc1anclem2  32459  ftc1anclem4  32461  ftc1anclem5  32462  ftc1anclem6  32463  ftc1anclem8  32465
  Copyright terms: Public domain W3C validator