Definition df-itg 25857

Description: Define the full Lebesgue integral, for complex-valued functions to ℝ. The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of 𝑥↑2 from 0 to 1 is ∫(0[,]1)(𝑥↑2) d𝑥 = (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 25855 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 25855 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.)

Assertion

Ref	Expression
df-itg	⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))

Distinct variable groups:   𝑦,𝑘,𝐴   𝐵,𝑘,𝑦   𝑥,𝑘,𝑦

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-itg

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	citg 25852	. 2 class ∫𝐴𝐵 d𝑥
5		cc0 11128	. . . 4 class 0
6		c3 12324	. . . 4 class 3
7		cfz 13565	. . . 4 class ...
8	5, 6, 7	co 7417	. . 3 class (0...3)
9		ci 11130	. . . . 5 class i
10		vk	. . . . . 6 setvar 𝑘
11	10	cv 1569	. . . . 5 class 𝑘
12		cexp 14129	. . . . 5 class ↑
13	9, 11, 12	co 7417	. . . 4 class (i↑𝑘)
14		cr 11127	. . . . . 6 class ℝ
15		vy	. . . . . . 7 setvar 𝑦
16		cdiv 11899	. . . . . . . . 9 class /
17	3, 13, 16	co 7417	. . . . . . . 8 class (𝐵 / (i↑𝑘))
18		cre 15188	. . . . . . . 8 class ℜ
19	17, 18	cfv 6537	. . . . . . 7 class (ℜ‘(𝐵 / (i↑𝑘)))
20	1	cv 1569	. . . . . . . . . 10 class 𝑥
21	20, 2	wcel 2145	. . . . . . . . 9 wff 𝑥 ∈ 𝐴
22	15	cv 1569	. . . . . . . . . 10 class 𝑦
23		cle 11272	. . . . . . . . . 10 class ≤
24	5, 22, 23	wbr 5107	. . . . . . . . 9 wff 0 ≤ 𝑦
25	21, 24	wa 401	. . . . . . . 8 wff (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦)
26	25, 22, 5	cif 4485	. . . . . . 7 class if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	15, 19, 26	csb 3850	. . . . . 6 class ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
28	1, 14, 27	cmpt 5190	. . . . 5 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))
29		citg2 25850	. . . . 5 class ∫2
30	28, 29	cfv 6537	. . . 4 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))
31		cmul 11133	. . . 4 class ·
32	13, 30, 31	co 7417	. . 3 class ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
33	8, 32, 10	csu 15777	. 2 class Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
34	4, 33	wceq 1570	1 wff ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))

This definition is used by:  dfitg  26003  itgex  26004  itgeq1f  26005  itgeq1  26007  nfitg1  26008  cbvitgv  26011  itgeq12i  36834  itgeq12sdv  36847  cbvitgvw2  36876  cbvitgdavw  36909  cbvitgdavw2  36925