Definition df-itg 24768

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 24766 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 24766 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 24763	. 2 class ∫𝐴𝐵 d𝑥
5		cc0 10855	. . . 4 class 0
6		c3 12012	. . . 4 class 3
7		cfz 13221	. . . 4 class ...
8	5, 6, 7	co 7268	. . 3 class (0...3)
9		ci 10857	. . . . 5 class i
10		vk	. . . . . 6 setvar 𝑘
11	10	cv 1540	. . . . 5 class 𝑘
12		cexp 13763	. . . . 5 class ↑
13	9, 11, 12	co 7268	. . . 4 class (i↑𝑘)
14		cr 10854	. . . . . 6 class ℝ
15		vy	. . . . . . 7 setvar 𝑦
16		cdiv 11615	. . . . . . . . 9 class /
17	3, 13, 16	co 7268	. . . . . . . 8 class (𝐵 / (i↑𝑘))
18		cre 14789	. . . . . . . 8 class ℜ
19	17, 18	cfv 6430	. . . . . . 7 class (ℜ‘(𝐵 / (i↑𝑘)))
20	1	cv 1540	. . . . . . . . . 10 class 𝑥
21	20, 2	wcel 2109	. . . . . . . . 9 wff 𝑥 ∈ 𝐴
22	15	cv 1540	. . . . . . . . . 10 class 𝑦
23		cle 10994	. . . . . . . . . 10 class ≤
24	5, 22, 23	wbr 5078	. . . . . . . . 9 wff 0 ≤ 𝑦
25	21, 24	wa 395	. . . . . . . 8 wff (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦)
26	25, 22, 5	cif 4464	. . . . . . 7 class if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	15, 19, 26	csb 3836	. . . . . 6 class ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)
28	1, 14, 27	cmpt 5161	. . . . 5 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))
29		citg2 24761	. . . . 5 class ∫2
30	28, 29	cfv 6430	. . . 4 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))
31		cmul 10860	. . . 4 class ·
32	13, 30, 31	co 7268	. . 3 class ((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
33	8, 32, 10	csu 15378	. 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  24915  itgex  24916  nfitg1  24919