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 · ( 𝑇 − 𝑈 ) ) ) )