Metamath Proof Explorer

Theorem itgcnlem

Description: Expand out the sum in dfitg . (Contributed by Mario Carneiro, 1-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itgcnlem.r ⊢ 𝑅 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.s ⊢ 𝑆 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.t ⊢ 𝑇 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.u ⊢ 𝑈 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgcnlem.i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
Assertion itgcnlem ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ( 𝑅 − 𝑆 ) + ( i · ( 𝑇 − 𝑈 ) ) ) )

Proof

Step Hyp Ref Expression
1 itgcnlem.r ⊢ 𝑅 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
2 itgcnlem.s ⊢ 𝑆 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
3 itgcnlem.t ⊢ 𝑇 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
4 itgcnlem.u ⊢ 𝑈 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
5 itgcnlem.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
6 itgcnlem.i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
7 eqid ⊢ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) )
8 7 dfitg ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
9 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10 df-3 ⊢ 3 = ( 2 + 1 )
11 oveq2 ⊢ ( 𝑘 = 3 → ( i ↑ 𝑘 ) = ( i ↑ 3 ) )
12 i3 ⊢ ( i ↑ 3 ) = - i
13 11 12 eqtrdi ⊢ ( 𝑘 = 3 → ( i ↑ 𝑘 ) = - i )
14 12 itgvallem ⊢ ( 𝑘 = 3 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) )
15 13 14 oveq12d ⊢ ( 𝑘 = 3 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( - i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ) )
16 ax-icn ⊢ i ∈ ℂ
17 16 a1i ⊢ ( 𝜑 → i ∈ ℂ )
18 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
19 17 18 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
20 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
21 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
23 21 22 6 5 iblitg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
24 23 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℂ )
25 20 24 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℂ )
26 19 25 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ∈ ℂ )
27 df-2 ⊢ 2 = ( 1 + 1 )
28 oveq2 ⊢ ( 𝑘 = 2 → ( i ↑ 𝑘 ) = ( i ↑ 2 ) )
29 i2 ⊢ ( i ↑ 2 ) = - 1
30 28 29 eqtrdi ⊢ ( 𝑘 = 2 → ( i ↑ 𝑘 ) = - 1 )
31 29 itgvallem ⊢ ( 𝑘 = 2 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) )
32 30 31 oveq12d ⊢ ( 𝑘 = 2 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( - 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ) )
33 1e0p1 ⊢ 1 = ( 0 + 1 )
34 oveq2 ⊢ ( 𝑘 = 1 → ( i ↑ 𝑘 ) = ( i ↑ 1 ) )
35 exp1 ⊢ ( i ∈ ℂ → ( i ↑ 1 ) = i )
36 16 35 ax-mp ⊢ ( i ↑ 1 ) = i
37 34 36 eqtrdi ⊢ ( 𝑘 = 1 → ( i ↑ 𝑘 ) = i )
38 36 itgvallem ⊢ ( 𝑘 = 1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) )
39 37 38 oveq12d ⊢ ( 𝑘 = 1 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ) )
40 0z ⊢ 0 ∈ ℤ
41 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
42 6 41 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
43 42 5 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
44 43 div1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 1 ) = 𝐵 )
45 44 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / 1 ) ) = ( ℜ ‘ 𝐵 ) )
46 45 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) )
47 46 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
48 47 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) )
49 1 48 eqtr4id ⊢ ( 𝜑 → 𝑅 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) )
50 49 oveq2d ⊢ ( 𝜑 → ( 1 · 𝑅 ) = ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) )
51 1 2 3 4 5 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )
52 6 51 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) )
53 52 simp2d ⊢ ( 𝜑 → ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) )
54 53 simpld ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
55 54 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
56 55 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑅 ) = 𝑅 )
57 50 56 eqtr3d ⊢ ( 𝜑 → ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) = 𝑅 )
58 57 55 eqeltrd ⊢ ( 𝜑 → ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) ∈ ℂ )
59 oveq2 ⊢ ( 𝑘 = 0 → ( i ↑ 𝑘 ) = ( i ↑ 0 ) )
60 exp0 ⊢ ( i ∈ ℂ → ( i ↑ 0 ) = 1 )
61 16 60 ax-mp ⊢ ( i ↑ 0 ) = 1
62 59 61 eqtrdi ⊢ ( 𝑘 = 0 → ( i ↑ 𝑘 ) = 1 )
63 61 itgvallem ⊢ ( 𝑘 = 0 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) )
64 62 63 oveq12d ⊢ ( 𝑘 = 0 → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) )
65 64 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) )
66 40 58 65 sylancr ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ) )
67 66 57 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = 𝑅 )
68 0nn0 ⊢ 0 ∈ ℕ0
69 67 68 jctil ⊢ ( 𝜑 → ( 0 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 0 ... 0 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = 𝑅 ) )
70 imval ⊢ ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / i ) ) )
71 43 70 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / i ) ) )
72 71 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) )
73 72 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) )
74 73 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) )
75 3 74 eqtr2id ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) = 𝑇 )
76 75 oveq2d ⊢ ( 𝜑 → ( i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ) = ( i · 𝑇 ) )
77 76 oveq2d ⊢ ( 𝜑 → ( 𝑅 + ( i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ) ) = ( 𝑅 + ( i · 𝑇 ) ) )
78 9 33 39 26 69 77 fsump1i ⊢ ( 𝜑 → ( 1 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( 𝑅 + ( i · 𝑇 ) ) ) )
79 43 renegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ - 𝐵 ) = - ( ℜ ‘ 𝐵 ) )
80 ax-1cn ⊢ 1 ∈ ℂ
81 80 negnegi ⊢ - - 1 = 1
82 81 oveq2i ⊢ ( - 𝐵 / - - 1 ) = ( - 𝐵 / 1 )
83 43 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℂ )
84 83 div1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / 1 ) = - 𝐵 )
85 82 84 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / - - 1 ) = - 𝐵 )
86 80 negcli ⊢ - 1 ∈ ℂ
87 neg1ne0 ⊢ - 1 ≠ 0
88 div2neg ⊢ ( ( 𝐵 ∈ ℂ ∧ - 1 ∈ ℂ ∧ - 1 ≠ 0 ) → ( - 𝐵 / - - 1 ) = ( 𝐵 / - 1 ) )
89 86 87 88 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( - 𝐵 / - - 1 ) = ( 𝐵 / - 1 ) )
90 43 89 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / - - 1 ) = ( 𝐵 / - 1 ) )
91 85 90 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 = ( 𝐵 / - 1 ) )
92 91 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ - 𝐵 ) = ( ℜ ‘ ( 𝐵 / - 1 ) ) )
93 79 92 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / - 1 ) ) )
94 93 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) )
95 94 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) )
96 95 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) )
97 2 96 eqtrid ⊢ ( 𝜑 → 𝑆 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) )
98 97 oveq2d ⊢ ( 𝜑 → ( - 1 · 𝑆 ) = ( - 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ) )
99 53 simprd ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
100 99 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
101 100 mulm1d ⊢ ( 𝜑 → ( - 1 · 𝑆 ) = - 𝑆 )
102 98 101 eqtr3d ⊢ ( 𝜑 → ( - 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ) = - 𝑆 )
103 102 oveq2d ⊢ ( 𝜑 → ( ( 𝑅 + ( i · 𝑇 ) ) + ( - 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ) ) = ( ( 𝑅 + ( i · 𝑇 ) ) + - 𝑆 ) )
104 52 simp3d ⊢ ( 𝜑 → ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) )
105 104 simpld ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
106 105 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
107 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( i · 𝑇 ) ∈ ℂ )
108 16 106 107 sylancr ⊢ ( 𝜑 → ( i · 𝑇 ) ∈ ℂ )
109 55 108 addcld ⊢ ( 𝜑 → ( 𝑅 + ( i · 𝑇 ) ) ∈ ℂ )
110 109 100 negsubd ⊢ ( 𝜑 → ( ( 𝑅 + ( i · 𝑇 ) ) + - 𝑆 ) = ( ( 𝑅 + ( i · 𝑇 ) ) − 𝑆 ) )
111 55 108 100 addsubd ⊢ ( 𝜑 → ( ( 𝑅 + ( i · 𝑇 ) ) − 𝑆 ) = ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) )
112 103 110 111 3eqtrd ⊢ ( 𝜑 → ( ( 𝑅 + ( i · 𝑇 ) ) + ( - 1 · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ) ) = ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) )
113 9 27 32 26 78 112 fsump1i ⊢ ( 𝜑 → ( 2 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 0 ... 2 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) ) )
114 imval ⊢ ( - 𝐵 ∈ ℂ → ( ℑ ‘ - 𝐵 ) = ( ℜ ‘ ( - 𝐵 / i ) ) )
115 83 114 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ - 𝐵 ) = ( ℜ ‘ ( - 𝐵 / i ) ) )
116 43 imnegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ - 𝐵 ) = - ( ℑ ‘ 𝐵 ) )
117 16 negnegi ⊢ - - i = i
118 117 eqcomi ⊢ i = - - i
119 118 oveq2i ⊢ ( - 𝐵 / i ) = ( - 𝐵 / - - i )
120 16 negcli ⊢ - i ∈ ℂ
121 ine0 ⊢ i ≠ 0
122 16 121 negne0i ⊢ - i ≠ 0
123 div2neg ⊢ ( ( 𝐵 ∈ ℂ ∧ - i ∈ ℂ ∧ - i ≠ 0 ) → ( - 𝐵 / - - i ) = ( 𝐵 / - i ) )
124 120 122 123 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( - 𝐵 / - - i ) = ( 𝐵 / - i ) )
125 43 124 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / - - i ) = ( 𝐵 / - i ) )
126 119 125 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / i ) = ( 𝐵 / - i ) )
127 126 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( - 𝐵 / i ) ) = ( ℜ ‘ ( 𝐵 / - i ) ) )
128 115 116 127 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / - i ) ) )
129 128 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) )
130 129 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) )
131 130 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) )
132 4 131 eqtrid ⊢ ( 𝜑 → 𝑈 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) )
133 132 oveq2d ⊢ ( 𝜑 → ( - i · 𝑈 ) = ( - i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ) )
134 104 simprd ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
135 134 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
136 mulneg12 ⊢ ( ( i ∈ ℂ ∧ 𝑈 ∈ ℂ ) → ( - i · 𝑈 ) = ( i · - 𝑈 ) )
137 16 135 136 sylancr ⊢ ( 𝜑 → ( - i · 𝑈 ) = ( i · - 𝑈 ) )
138 133 137 eqtr3d ⊢ ( 𝜑 → ( - i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ) = ( i · - 𝑈 ) )
139 138 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) + ( - i · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ) ) = ( ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) + ( i · - 𝑈 ) ) )
140 9 10 15 26 113 139 fsump1i ⊢ ( 𝜑 → ( 3 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) + ( i · - 𝑈 ) ) ) )
141 140 simprd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) + ( i · - 𝑈 ) ) )
142 8 141 eqtrid ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) + ( i · - 𝑈 ) ) )
143 55 100 subcld ⊢ ( 𝜑 → ( 𝑅 − 𝑆 ) ∈ ℂ )
144 135 negcld ⊢ ( 𝜑 → - 𝑈 ∈ ℂ )
145 mulcl ⊢ ( ( i ∈ ℂ ∧ - 𝑈 ∈ ℂ ) → ( i · - 𝑈 ) ∈ ℂ )
146 16 144 145 sylancr ⊢ ( 𝜑 → ( i · - 𝑈 ) ∈ ℂ )
147 143 108 146 addassd ⊢ ( 𝜑 → ( ( ( 𝑅 − 𝑆 ) + ( i · 𝑇 ) ) + ( i · - 𝑈 ) ) = ( ( 𝑅 − 𝑆 ) + ( ( i · 𝑇 ) + ( i · - 𝑈 ) ) ) )
148 17 106 144 adddid ⊢ ( 𝜑 → ( i · ( 𝑇 + - 𝑈 ) ) = ( ( i · 𝑇 ) + ( i · - 𝑈 ) ) )
149 106 135 negsubd ⊢ ( 𝜑 → ( 𝑇 + - 𝑈 ) = ( 𝑇 − 𝑈 ) )
150 149 oveq2d ⊢ ( 𝜑 → ( i · ( 𝑇 + - 𝑈 ) ) = ( i · ( 𝑇 − 𝑈 ) ) )
151 148 150 eqtr3d ⊢ ( 𝜑 → ( ( i · 𝑇 ) + ( i · - 𝑈 ) ) = ( i · ( 𝑇 − 𝑈 ) ) )
152 151 oveq2d ⊢ ( 𝜑 → ( ( 𝑅 − 𝑆 ) + ( ( i · 𝑇 ) + ( i · - 𝑈 ) ) ) = ( ( 𝑅 − 𝑆 ) + ( i · ( 𝑇 − 𝑈 ) ) ) )
153 142 147 152 3eqtrd ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ( 𝑅 − 𝑆 ) + ( i · ( 𝑇 − 𝑈 ) ) ) )