Theorem iblmbf 25695

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047  ⦋csb 3845  ifcif 4472   class class class wbr 5089   ↦ cmpt 5170  dom cdm 5614  ‘cfv 6481  (class class class)co 7346  ℝcr 11005  0cc0 11006  ici 11008   ≤ cle 11147   / cdiv 11774  3c3 12181  ...cfz 13407  ↑cexp 13968  ℜcre 15004  MblFncmbf 25542  ∫₂citg2 25544  𝐿¹cibl 25545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-ibl 25550

This theorem is referenced by:  iblcnlem  25717  itgcnlem  25718  itgcnval  25728  itgre  25729  itgim  25730  iblneg  25731  itgneg  25732  iblss  25733  iblss2  25734  itgge0  25739  itgss3  25743  itgless  25745  iblsub  25750  itgadd  25753  itgsub  25754  itgfsum  25755  iblabs  25757  iblmulc2  25759  itgmulc2  25762  itgabs  25763  itgsplit  25764  bddmulibl  25767  itggt0  25772  itgcn  25773  ditgswap  25787  ditgsplitlem  25788  ftc1a  25971  itgsubstlem  25982  iblulm  26343  itgulm  26344  ibladdnc  37716  itgaddnclem1  37717  itgaddnclem2  37718  itgaddnc  37719  iblsubnc  37720  itgsubnc  37721  iblabsnclem  37722  iblabsnc  37723  iblmulc2nc  37724  itgmulc2nclem2  37726  itgmulc2nc  37727  itgabsnc  37728  ftc1cnnclem  37730  ftc1anclem2  37733  ftc1anclem4  37735  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem8  37739