Theorem iblmbf 25831

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.

Step	Hyp	Ref	Expression
1		df-ibl 25686	. . 3 ⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2	1	ssrab3 4037	. 2 ⊢ 𝐿1 ⊆ MblFn
3	2	sseli 3934	1 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ∀wral 3078  ⦋csb 3854  ifcif 4482   class class class wbr 5102   ↦ cmpt 5183  dom cdm 5649  ‘cfv 6523  (class class class)co 7398  ℝcr 11074  0cc0 11075  ici 11077   ≤ cle 11219   / cdiv 11846  3c3 12275  ...cfz 13514  ↑cexp 14076  ℜcre 15126  MblFncmbf 25678  ∫₂citg2 25680  𝐿¹cibl 25681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-ss 3923  df-ibl 25686

This theorem is referenced by:  iblcnlem  25853  itgcnlem  25854  itgcnval  25864  itgre  25865  itgim  25866  iblneg  25867  itgneg  25868  iblss  25869  iblss2  25870  itgge0  25875  itgss3  25879  itgless  25881  iblsub  25886  itgadd  25889  itgsub  25890  itgfsum  25891  iblabs  25893  iblmulc2  25895  itgmulc2  25898  itgabs  25899  itgsplit  25900  bddmulibl  25903  itggt0  25908  itgcn  25909  ditgswap  25923  ditgsplitlem  25924  ftc1a  26101  itgsubstlem  26112  iblulm  26472  itgulm  26473  ibladdnc  38181  itgaddnclem1  38182  itgaddnclem2  38183  itgaddnc  38184  iblsubnc  38185  itgsubnc  38186  iblabsnclem  38187  iblabsnc  38188  iblmulc2nc  38189  itgmulc2nclem2  38191  itgmulc2nc  38192  itgabsnc  38193  ftc1cnnclem  38195  ftc1anclem2  38198  ftc1anclem4  38200  ftc1anclem5  38201  ftc1anclem6  38202  ftc1anclem8  38204