Definition df-itg 25544

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 25542 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 25542 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 25539	. 2 class ∫𝐴𝐵 d𝑥
5		cc0 10998	. . . 4 class 0
6		c3 12173	. . . 4 class 3
7		cfz 13399	. . . 4 class ...
8	5, 6, 7	co 7341	. . 3 class (0...3)
9		ci 11000	. . . . 5 class i
10		vk	. . . . . 6 setvar 𝑘
11	10	cv 1540	. . . . 5 class 𝑘
12		cexp 13960	. . . . 5 class ↑
13	9, 11, 12	co 7341	. . . 4 class (i↑𝑘)
14		cr 10997	. . . . . 6 class ℝ
15		vy	. . . . . . 7 setvar 𝑦
16		cdiv 11766	. . . . . . . . 9 class /
17	3, 13, 16	co 7341	. . . . . . . 8 class (𝐵 / (i↑𝑘))
18		cre 14996	. . . . . . . 8 class ℜ
19	17, 18	cfv 6477	. . . . . . 7 class (ℜ‘(𝐵 / (i↑𝑘)))
20	1	cv 1540	. . . . . . . . . 10 class 𝑥
21	20, 2	wcel 2110	. . . . . . . . 9 wff 𝑥 ∈ 𝐴
22	15	cv 1540	. . . . . . . . . 10 class 𝑦
23		cle 11139	. . . . . . . . . 10 class ≤
24	5, 22, 23	wbr 5089	. . . . . . . . 9 wff 0 ≤ 𝑦
25	21, 24	wa 395	. . . . . . . 8 wff (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦)
26	25, 22, 5	cif 4473	. . . . . . 7 class if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	15, 19, 26	csb 3848	. . . . . 6 class ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
28	1, 14, 27	cmpt 5170	. . . . 5 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))
29		citg2 25537	. . . . 5 class ∫2
30	28, 29	cfv 6477	. . . 4 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))
31		cmul 11003	. . . 4 class ·
32	13, 30, 31	co 7341	. . 3 class ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
33	8, 32, 10	csu 15585	. 2 class Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
34	4, 33	wceq 1541	1 wff ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))

This definition is referenced by:  dfitg  25690  itgex  25691  itgeq1f  25692  itgeq1  25694  nfitg1  25695  cbvitgv  25698  itgeq12i  36219  itgeq12sdv  36232  cbvitgvw2  36261  cbvitgdavw  36294  cbvitgdavw2  36310