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}Bdx=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}Bdx=\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	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\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	eqtrdi	$$⊢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 {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
19	17 18	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
20		nn0z	$$⊢k\in {\mathbb{N}}_0\to k\in \mathbb{Z}$$
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 \mathbb{Z}\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 \mathbb{Z}\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 {\mathbb{N}}_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 {\mathbb{N}}_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	eqtrdi	$$⊢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	eqtrdi	$$⊢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 \mathbb{Z}$$
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	1 48	eqtr4id	$$⊢\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 1R=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\leftrightarrow \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 1R=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	eqtrdi	$$⊢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 \mathbb{Z}\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 {\mathbb{N}}_0$$
69	67 68	jctil	$$⊢\phi \to \left(0\in {\mathbb{N}}_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 {\mathbb{N}}_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 -1S=-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 -1S=-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 {\mathbb{N}}_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 {\mathbb{N}}_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}Bdx=\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}Bdx=R-S+\mathrm{i}\left(T-U\right)$$