Definition df-itg

Description: Define the full Lebesgue integral, for complex-valued functions to RR . The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of x ^ 2 from 0 to 1 is S. ( 0 , 1 ) ( x ^ 2 ) _d x = ( 1 / 3 ) . The only real function of this definition is to break the integral up into nonnegative real parts and send it off to df-itg2 for further processing. Note that this definition cannot handle integrals which evaluate to infinity, because addition and multiplication are not currently defined on extended reals. (You can use df-itg2 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	df-itg	$$⊢{\int }_{A}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		vx	$$setvarx$$
3	2 0 1	citg	$$class{\int }_{A}Bdx$$
4		vk	$$setvark$$
5		cc0	$$class0$$
6		cfz	$$class\dots$$
7		c3	$$class3$$
8	5 7 6	co	$$class\left(0\dots 3\right)$$
9		ci	$$class\mathrm{i}$$
10		cexp	$$class^$$
11	4	cv	$$setvark$$
12	9 11 10	co	$$class{\mathrm{i}}^k$$
13		cmul	$$class\times$$
14		citg2	$$class{\int }^2$$
15		cr	$$classℝ$$
16		cre	$$class\Re$$
17		cdiv	$$class÷$$
18	1 12 17	co	$$class\left(\frac{B}{{\mathrm{i}}^k}\right)$$
19	18 16	cfv	$$class\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
20		vy	$$setvary$$
21	2	cv	$$setvarx$$
22	21 0	wcel	$$wffx\in A$$
23		cle	$$class\le$$
24	20	cv	$$setvary$$
25	5 24 23	wbr	$$wff0\le y$$
26	22 25	wa	$$wff\left(x\in A\wedge 0\le y\right)$$
27	26 24 5	cif	$$classif\left(\left(x\in A\wedge 0\le y\right),y,0\right)$$
28	20 19 27	csb	$$class⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)$$
29	2 15 28	cmpt	$$class\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)$$
30	29 14	cfv	$$class{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$
31	12 30 13	co	$$class{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$
32	8 31 4	csu	$$class\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$
33	3 32	wceq	$$wff{\int }_{A}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$