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 syl5eq ( ( 𝜑𝑥𝐴 ) → ( - 𝐵 / - - 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 syl5eq ( 𝜑𝑆 = ( ∫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 syl5eq ( ( 𝜑𝑥𝐴 ) → ( - 𝐵 / 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 syl5eq ( 𝜑𝑈 = ( ∫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 syl5eq ( 𝜑 → ∫ 𝐴 𝐵 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 · ( 𝑇𝑈 ) ) ) )