Definition df-ibl

Description: Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	df-ibl	$$⊢{𝐿}^1=\left\{f\in MblFn|\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cibl	$$class{𝐿}^1$$
1		vf	$$setvarf$$
2		cmbf	$$classMblFn$$
3		vk	$$setvark$$
4		cc0	$$class0$$
5		cfz	$$class\dots$$
6		c3	$$class3$$
7	4 6 5	co	$$class\left(0\dots 3\right)$$
8		citg2	$$class{\int }^2$$
9		vx	$$setvarx$$
10		cr	$$classℝ$$
11		cre	$$class\Re$$
12	1	cv	$$setvarf$$
13	9	cv	$$setvarx$$
14	13 12	cfv	$$classf\left(x\right)$$
15		cdiv	$$class÷$$
16		ci	$$class\mathrm{i}$$
17		cexp	$$class^$$
18	3	cv	$$setvark$$
19	16 18 17	co	$$class{\mathrm{i}}^k$$
20	14 19 15	co	$$class\left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)$$
21	20 11	cfv	$$class\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)$$
22		vy	$$setvary$$
23	12	cdm	$$class\mathrm{dom}f$$
24	13 23	wcel	$$wffx\in \mathrm{dom}f$$
25		cle	$$class\le$$
26	22	cv	$$setvary$$
27	4 26 25	wbr	$$wff0\le y$$
28	24 27	wa	$$wff\left(x\in \mathrm{dom}f\wedge 0\le y\right)$$
29	28 26 4	cif	$$classif\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)$$
30	22 21 29	csb	$$class⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)$$
31	9 10 30	cmpt	$$class\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)$$
32	31 8	cfv	$$class{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)$$
33	32 10	wcel	$$wff{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ$$
34	33 3 7	wral	$$wff\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ$$
35	34 1 2	crab	$$class\left\{f\in MblFn|\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\right\}$$
36	0 35	wceq	$$wff{𝐿}^1=\left\{f\in MblFn|\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\right\}$$