Theorem iblmbf 25666

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 25521	. . 3 ⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2	1	ssrab3 4033	. 2 ⊢ 𝐿1 ⊆ MblFn
3	2	sseli 3931	1 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  ⦋csb 3851  ifcif 4476   class class class wbr 5092   ↦ cmpt 5173  dom cdm 5619  ‘cfv 6482  (class class class)co 7349  ℝcr 11008  0cc0 11009  ici 11011   ≤ cle 11150   / cdiv 11777  3c3 12184  ...cfz 13410  ↑cexp 13968  ℜcre 15004  MblFncmbf 25513  ∫₂citg2 25515  𝐿¹cibl 25516

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-ss 3920  df-ibl 25521

This theorem is referenced by:  iblcnlem  25688  itgcnlem  25689  itgcnval  25699  itgre  25700  itgim  25701  iblneg  25702  itgneg  25703  iblss  25704  iblss2  25705  itgge0  25710  itgss3  25714  itgless  25716  iblsub  25721  itgadd  25724  itgsub  25725  itgfsum  25726  iblabs  25728  iblmulc2  25730  itgmulc2  25733  itgabs  25734  itgsplit  25735  bddmulibl  25738  itggt0  25743  itgcn  25744  ditgswap  25758  ditgsplitlem  25759  ftc1a  25942  itgsubstlem  25953  iblulm  26314  itgulm  26315  ibladdnc  37667  itgaddnclem1  37668  itgaddnclem2  37669  itgaddnc  37670  iblsubnc  37671  itgsubnc  37672  iblabsnclem  37673  iblabsnc  37674  iblmulc2nc  37675  itgmulc2nclem2  37677  itgmulc2nc  37678  itgabsnc  37679  ftc1cnnclem  37681  ftc1anclem2  37684  ftc1anclem4  37686  ftc1anclem5  37687  ftc1anclem6  37688  ftc1anclem8  37690