Theorem iblmbf 25816

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058  ⦋csb 3907  ifcif 4530   class class class wbr 5147   ↦ cmpt 5230  dom cdm 5688  ‘cfv 6562  (class class class)co 7430  ℝcr 11151  0cc0 11152  ici 11154   ≤ cle 11293   / cdiv 11917  3c3 12319  ...cfz 13543  ↑cexp 14098  ℜcre 15132  MblFncmbf 25662  ∫₂citg2 25664  𝐿¹cibl 25665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-ss 3979  df-ibl 25670

This theorem is referenced by:  iblcnlem  25838  itgcnlem  25839  itgcnval  25849  itgre  25850  itgim  25851  iblneg  25852  itgneg  25853  iblss  25854  iblss2  25855  itgge0  25860  itgss3  25864  itgless  25866  iblsub  25871  itgadd  25874  itgsub  25875  itgfsum  25876  iblabs  25878  iblmulc2  25880  itgmulc2  25883  itgabs  25884  itgsplit  25885  bddmulibl  25888  itggt0  25893  itgcn  25894  ditgswap  25908  ditgsplitlem  25909  ftc1a  26092  itgsubstlem  26103  iblulm  26464  itgulm  26465  ibladdnc  37663  itgaddnclem1  37664  itgaddnclem2  37665  itgaddnc  37666  iblsubnc  37667  itgsubnc  37668  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nclem2  37673  itgmulc2nc  37674  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem2  37680  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem8  37686