# 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}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)$
itgcnlem.s ${⊢}{S}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)$
itgcnlem.t ${⊢}{T}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)$
itgcnlem.u ${⊢}{U}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)$
itgcnlem.v ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
itgcnlem.i ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
Assertion itgcnlem ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={R}-{S}+\mathrm{i}\left({T}-{U}\right)$

### Proof

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