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 
|- R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
itgcnlem.s 
|- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
itgcnlem.t 
|- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
itgcnlem.u 
|- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
itgcnlem.v 
|- ( ( ph /\ x e. A ) -> B e. V )
itgcnlem.i 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion itgcnlem 
|- ( ph -> S. A B _d x = ( ( R - S ) + ( _i x. ( T - U ) ) ) )

Proof

Step Hyp Ref Expression
1 itgcnlem.r 
 |-  R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
2 itgcnlem.s 
 |-  S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
3 itgcnlem.t 
 |-  T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
4 itgcnlem.u 
 |-  U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
5 itgcnlem.v 
 |-  ( ( ph /\ x e. A ) -> B e. V )
6 itgcnlem.i 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
7 eqid 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) )
8 7 dfitg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 df-3 
 |-  3 = ( 2 + 1 )
11 oveq2 
 |-  ( k = 3 -> ( _i ^ k ) = ( _i ^ 3 ) )
12 i3 
 |-  ( _i ^ 3 ) = -u _i
13 11 12 eqtrdi 
 |-  ( k = 3 -> ( _i ^ k ) = -u _i )
14 12 itgvallem 
 |-  ( k = 3 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) )
15 13 14 oveq12d 
 |-  ( k = 3 -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( -u _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) ) )
16 ax-icn 
 |-  _i e. CC
17 16 a1i 
 |-  ( ph -> _i e. CC )
18 expcl 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
19 17 18 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
20 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
21 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
22 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
23 21 22 6 5 iblitg 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
24 23 recnd 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. CC )
25 20 24 sylan2 
 |-  ( ( ph /\ k e. NN0 ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. CC )
26 19 25 mulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) e. CC )
27 df-2 
 |-  2 = ( 1 + 1 )
28 oveq2 
 |-  ( k = 2 -> ( _i ^ k ) = ( _i ^ 2 ) )
29 i2 
 |-  ( _i ^ 2 ) = -u 1
30 28 29 eqtrdi 
 |-  ( k = 2 -> ( _i ^ k ) = -u 1 )
31 29 itgvallem 
 |-  ( k = 2 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) )
32 30 31 oveq12d 
 |-  ( k = 2 -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( -u 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) ) )
33 1e0p1 
 |-  1 = ( 0 + 1 )
34 oveq2 
 |-  ( k = 1 -> ( _i ^ k ) = ( _i ^ 1 ) )
35 exp1 
 |-  ( _i e. CC -> ( _i ^ 1 ) = _i )
36 16 35 ax-mp 
 |-  ( _i ^ 1 ) = _i
37 34 36 eqtrdi 
 |-  ( k = 1 -> ( _i ^ k ) = _i )
38 36 itgvallem 
 |-  ( k = 1 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) )
39 37 38 oveq12d 
 |-  ( k = 1 -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) ) )
40 0z 
 |-  0 e. ZZ
41 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
42 6 41 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
43 42 5 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
44 43 div1d 
 |-  ( ( ph /\ x e. A ) -> ( B / 1 ) = B )
45 44 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / 1 ) ) = ( Re ` B ) )
46 45 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) )
47 46 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
48 47 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) )
49 1 48 eqtr4id 
 |-  ( ph -> R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) )
50 49 oveq2d 
 |-  ( ph -> ( 1 x. R ) = ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) )
51 1 2 3 4 5 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )
52 6 51 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) )
53 52 simp2d 
 |-  ( ph -> ( R e. RR /\ S e. RR ) )
54 53 simpld 
 |-  ( ph -> R e. RR )
55 54 recnd 
 |-  ( ph -> R e. CC )
56 55 mulid2d 
 |-  ( ph -> ( 1 x. R ) = R )
57 50 56 eqtr3d 
 |-  ( ph -> ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) = R )
58 57 55 eqeltrd 
 |-  ( ph -> ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) e. CC )
59 oveq2 
 |-  ( k = 0 -> ( _i ^ k ) = ( _i ^ 0 ) )
60 exp0 
 |-  ( _i e. CC -> ( _i ^ 0 ) = 1 )
61 16 60 ax-mp 
 |-  ( _i ^ 0 ) = 1
62 59 61 eqtrdi 
 |-  ( k = 0 -> ( _i ^ k ) = 1 )
63 61 itgvallem 
 |-  ( k = 0 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) )
64 62 63 oveq12d 
 |-  ( k = 0 -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) )
65 64 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) )
66 40 58 65 sylancr 
 |-  ( ph -> sum_ k e. ( 0 ... 0 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) ) )
67 66 57 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... 0 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = R )
68 0nn0 
 |-  0 e. NN0
69 67 68 jctil 
 |-  ( ph -> ( 0 e. NN0 /\ sum_ k e. ( 0 ... 0 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = R ) )
70 imval 
 |-  ( B e. CC -> ( Im ` B ) = ( Re ` ( B / _i ) ) )
71 43 70 syl 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) = ( Re ` ( B / _i ) ) )
72 71 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) )
73 72 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) )
74 73 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) )
75 3 74 syl5req 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) = T )
76 75 oveq2d 
 |-  ( ph -> ( _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) ) = ( _i x. T ) )
77 76 oveq2d 
 |-  ( ph -> ( R + ( _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) ) ) = ( R + ( _i x. T ) ) )
78 9 33 39 26 69 77 fsump1i 
 |-  ( ph -> ( 1 e. NN0 /\ sum_ k e. ( 0 ... 1 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( R + ( _i x. T ) ) ) )
79 43 renegd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) = -u ( Re ` B ) )
80 ax-1cn 
 |-  1 e. CC
81 80 negnegi 
 |-  -u -u 1 = 1
82 81 oveq2i 
 |-  ( -u B / -u -u 1 ) = ( -u B / 1 )
83 43 negcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
84 83 div1d 
 |-  ( ( ph /\ x e. A ) -> ( -u B / 1 ) = -u B )
85 82 84 syl5eq 
 |-  ( ( ph /\ x e. A ) -> ( -u B / -u -u 1 ) = -u B )
86 80 negcli 
 |-  -u 1 e. CC
87 neg1ne0 
 |-  -u 1 =/= 0
88 div2neg 
 |-  ( ( B e. CC /\ -u 1 e. CC /\ -u 1 =/= 0 ) -> ( -u B / -u -u 1 ) = ( B / -u 1 ) )
89 86 87 88 mp3an23 
 |-  ( B e. CC -> ( -u B / -u -u 1 ) = ( B / -u 1 ) )
90 43 89 syl 
 |-  ( ( ph /\ x e. A ) -> ( -u B / -u -u 1 ) = ( B / -u 1 ) )
91 85 90 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> -u B = ( B / -u 1 ) )
92 91 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) = ( Re ` ( B / -u 1 ) ) )
93 79 92 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` B ) = ( Re ` ( B / -u 1 ) ) )
94 93 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) )
95 94 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) )
96 95 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) )
97 2 96 syl5eq 
 |-  ( ph -> S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) )
98 97 oveq2d 
 |-  ( ph -> ( -u 1 x. S ) = ( -u 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) ) )
99 53 simprd 
 |-  ( ph -> S e. RR )
100 99 recnd 
 |-  ( ph -> S e. CC )
101 100 mulm1d 
 |-  ( ph -> ( -u 1 x. S ) = -u S )
102 98 101 eqtr3d 
 |-  ( ph -> ( -u 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) ) = -u S )
103 102 oveq2d 
 |-  ( ph -> ( ( R + ( _i x. T ) ) + ( -u 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) ) ) = ( ( R + ( _i x. T ) ) + -u S ) )
104 52 simp3d 
 |-  ( ph -> ( T e. RR /\ U e. RR ) )
105 104 simpld 
 |-  ( ph -> T e. RR )
106 105 recnd 
 |-  ( ph -> T e. CC )
107 mulcl 
 |-  ( ( _i e. CC /\ T e. CC ) -> ( _i x. T ) e. CC )
108 16 106 107 sylancr 
 |-  ( ph -> ( _i x. T ) e. CC )
109 55 108 addcld 
 |-  ( ph -> ( R + ( _i x. T ) ) e. CC )
110 109 100 negsubd 
 |-  ( ph -> ( ( R + ( _i x. T ) ) + -u S ) = ( ( R + ( _i x. T ) ) - S ) )
111 55 108 100 addsubd 
 |-  ( ph -> ( ( R + ( _i x. T ) ) - S ) = ( ( R - S ) + ( _i x. T ) ) )
112 103 110 111 3eqtrd 
 |-  ( ph -> ( ( R + ( _i x. T ) ) + ( -u 1 x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) ) ) = ( ( R - S ) + ( _i x. T ) ) )
113 9 27 32 26 78 112 fsump1i 
 |-  ( ph -> ( 2 e. NN0 /\ sum_ k e. ( 0 ... 2 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( R - S ) + ( _i x. T ) ) ) )
114 imval 
 |-  ( -u B e. CC -> ( Im ` -u B ) = ( Re ` ( -u B / _i ) ) )
115 83 114 syl 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) = ( Re ` ( -u B / _i ) ) )
116 43 imnegd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) = -u ( Im ` B ) )
117 16 negnegi 
 |-  -u -u _i = _i
118 117 eqcomi 
 |-  _i = -u -u _i
119 118 oveq2i 
 |-  ( -u B / _i ) = ( -u B / -u -u _i )
120 16 negcli 
 |-  -u _i e. CC
121 ine0 
 |-  _i =/= 0
122 16 121 negne0i 
 |-  -u _i =/= 0
123 div2neg 
 |-  ( ( B e. CC /\ -u _i e. CC /\ -u _i =/= 0 ) -> ( -u B / -u -u _i ) = ( B / -u _i ) )
124 120 122 123 mp3an23 
 |-  ( B e. CC -> ( -u B / -u -u _i ) = ( B / -u _i ) )
125 43 124 syl 
 |-  ( ( ph /\ x e. A ) -> ( -u B / -u -u _i ) = ( B / -u _i ) )
126 119 125 syl5eq 
 |-  ( ( ph /\ x e. A ) -> ( -u B / _i ) = ( B / -u _i ) )
127 126 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( -u B / _i ) ) = ( Re ` ( B / -u _i ) ) )
128 115 116 127 3eqtr3d 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) = ( Re ` ( B / -u _i ) ) )
129 128 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) )
130 129 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) )
131 130 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) )
132 4 131 syl5eq 
 |-  ( ph -> U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) )
133 132 oveq2d 
 |-  ( ph -> ( -u _i x. U ) = ( -u _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) ) )
134 104 simprd 
 |-  ( ph -> U e. RR )
135 134 recnd 
 |-  ( ph -> U e. CC )
136 mulneg12 
 |-  ( ( _i e. CC /\ U e. CC ) -> ( -u _i x. U ) = ( _i x. -u U ) )
137 16 135 136 sylancr 
 |-  ( ph -> ( -u _i x. U ) = ( _i x. -u U ) )
138 133 137 eqtr3d 
 |-  ( ph -> ( -u _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) ) = ( _i x. -u U ) )
139 138 oveq2d 
 |-  ( ph -> ( ( ( R - S ) + ( _i x. T ) ) + ( -u _i x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) ) ) = ( ( ( R - S ) + ( _i x. T ) ) + ( _i x. -u U ) ) )
140 9 10 15 26 113 139 fsump1i 
 |-  ( ph -> ( 3 e. NN0 /\ sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( ( R - S ) + ( _i x. T ) ) + ( _i x. -u U ) ) ) )
141 140 simprd 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) = ( ( ( R - S ) + ( _i x. T ) ) + ( _i x. -u U ) ) )
142 8 141 syl5eq 
 |-  ( ph -> S. A B _d x = ( ( ( R - S ) + ( _i x. T ) ) + ( _i x. -u U ) ) )
143 55 100 subcld 
 |-  ( ph -> ( R - S ) e. CC )
144 135 negcld 
 |-  ( ph -> -u U e. CC )
145 mulcl 
 |-  ( ( _i e. CC /\ -u U e. CC ) -> ( _i x. -u U ) e. CC )
146 16 144 145 sylancr 
 |-  ( ph -> ( _i x. -u U ) e. CC )
147 143 108 146 addassd 
 |-  ( ph -> ( ( ( R - S ) + ( _i x. T ) ) + ( _i x. -u U ) ) = ( ( R - S ) + ( ( _i x. T ) + ( _i x. -u U ) ) ) )
148 17 106 144 adddid 
 |-  ( ph -> ( _i x. ( T + -u U ) ) = ( ( _i x. T ) + ( _i x. -u U ) ) )
149 106 135 negsubd 
 |-  ( ph -> ( T + -u U ) = ( T - U ) )
150 149 oveq2d 
 |-  ( ph -> ( _i x. ( T + -u U ) ) = ( _i x. ( T - U ) ) )
151 148 150 eqtr3d 
 |-  ( ph -> ( ( _i x. T ) + ( _i x. -u U ) ) = ( _i x. ( T - U ) ) )
152 151 oveq2d 
 |-  ( ph -> ( ( R - S ) + ( ( _i x. T ) + ( _i x. -u U ) ) ) = ( ( R - S ) + ( _i x. ( T - U ) ) ) )
153 142 147 152 3eqtrd 
 |-  ( ph -> S. A B _d x = ( ( R - S ) + ( _i x. ( T - U ) ) ) )