Metamath Proof Explorer

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 ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ⊢ 𝐴
1 cB ⊢ 𝐵
2 vx ⊢ 𝑥
3 2 0 1 citg ⊢ ∫ 𝐴 𝐵 d 𝑥
4 vk ⊢ 𝑘
5 cc0 ⊢ 0
6 cfz ⊢ ...
7 c3 ⊢ 3
8 5 7 6 co ⊢ ( 0 ... 3 )
9 ci ⊢ i
10 cexp ⊢ ↑
11 4 cv ⊢ 𝑘
12 9 11 10 co ⊢ ( i ↑ 𝑘 )
13 cmul ⊢ ·
14 citg2 ⊢ ∫2
15 cr ⊢ ℝ
16 cre ⊢ ℜ
17 cdiv ⊢ /
18 1 12 17 co ⊢ ( 𝐵 / ( i ↑ 𝑘 ) )
19 18 16 cfv ⊢ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
20 vy ⊢ 𝑦
21 2 cv ⊢ 𝑥
22 21 0 wcel ⊢ 𝑥 ∈ 𝐴
23 cle ⊢ ≤
24 20 cv ⊢ 𝑦
25 5 24 23 wbr ⊢ 0 ≤ 𝑦
26 22 25 wa ⊢ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 )
27 26 24 5 cif ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
28 20 19 27 csb ⊢ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
29 2 15 28 cmpt ⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
30 29 14 cfv ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) )
31 12 30 13 co ⊢ ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
32 8 31 4 csu ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )
33 3 32 wceq ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) )