Definition df-itg 24218

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 24216 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 24216 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 24213	. 2 class ∫𝐴𝐵 d𝑥
5		cc0 10531	. . . 4 class 0
6		c3 11687	. . . 4 class 3
7		cfz 12886	. . . 4 class ...
8	5, 6, 7	co 7150	. . 3 class (0...3)
9		ci 10533	. . . . 5 class i
10		vk	. . . . . 6 setvar 𝑘
11	10	cv 1532	. . . . 5 class 𝑘
12		cexp 13423	. . . . 5 class ↑
13	9, 11, 12	co 7150	. . . 4 class (i↑𝑘)
14		cr 10530	. . . . . 6 class ℝ
15		vy	. . . . . . 7 setvar 𝑦
16		cdiv 11291	. . . . . . . . 9 class /
17	3, 13, 16	co 7150	. . . . . . . 8 class (𝐵 / (i↑𝑘))
18		cre 14450	. . . . . . . 8 class ℜ
19	17, 18	cfv 6349	. . . . . . 7 class (ℜ‘(𝐵 / (i↑𝑘)))
20	1	cv 1532	. . . . . . . . . 10 class 𝑥
21	20, 2	wcel 2110	. . . . . . . . 9 wff 𝑥 ∈ 𝐴
22	15	cv 1532	. . . . . . . . . 10 class 𝑦
23		cle 10670	. . . . . . . . . 10 class ≤
24	5, 22, 23	wbr 5058	. . . . . . . . 9 wff 0 ≤ 𝑦
25	21, 24	wa 398	. . . . . . . 8 wff (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦)
26	25, 22, 5	cif 4466	. . . . . . 7 class if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	15, 19, 26	csb 3882	. . . . . 6 class ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
28	1, 14, 27	cmpt 5138	. . . . 5 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))
29		citg2 24211	. . . . 5 class ∫2
30	28, 29	cfv 6349	. . . 4 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))
31		cmul 10536	. . . 4 class ·
32	13, 30, 31	co 7150	. . 3 class ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
33	8, 32, 10	csu 15036	. 2 class Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
34	4, 33	wceq 1533	1 wff ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))

This definition is referenced by:  dfitg  24364  itgex  24365  nfitg1  24368