Theorem itgmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	itgmulc2.1	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	itgmulc2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	itgmulc2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
Assertion	itgmulc2	⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgmulc2.1	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		itgmulc2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		itgmulc2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4	1	recld	⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℂ )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
7		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
9	8 2	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
10	9	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
11	10	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
12	6 11	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
13	9	iblcn	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
14	3 13	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
15	14	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
16	5 10 15	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
17	12 16	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
18		ax-icn	⊢ i ∈ ℂ
19	9	imcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
20	19	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
21	6 20	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
22	14	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
23	5 19 22	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
24	21 23	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
25		mulcl	⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
26	18 24 25	sylancr	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
27	1	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℝ )
28	27	renegcld	⊢ ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
29	28	recnd	⊢ ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℂ )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℂ )
31	30 20	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
32	29 19 22	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
33	31 32	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
34	27	recnd	⊢ ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℂ )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
36	35 11	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
37	34 10 15	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
38	36 37	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
39		mulcl	⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
40	18 38 39	sylancr	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
41	17 26 33 40	add4d	⊢ ( 𝜑 → ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
42	2 3	itgcl	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
43		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐶 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐶 ) ) ∈ ℂ )
44	18 34 43	sylancr	⊢ ( 𝜑 → ( i · ( ℑ ‘ 𝐶 ) ) ∈ ℂ )
45	2 3	itgcnval	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
46	45	oveq2d	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ℜ ‘ 𝐶 ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
47	10 15	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
48	19 22	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
49		mulcl	⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
50	18 48 49	sylancr	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
51	5 47 50	adddid	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
52	5 10 15 4 10	itgmulc2lem2	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 )
53	18	a1i	⊢ ( 𝜑 → i ∈ ℂ )
54	5 53 48	mul12d	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
55	5 19 22 4 19	itgmulc2lem2	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
56	55	oveq2d	⊢ ( 𝜑 → ( i · ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
57	54 56	eqtrd	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
58	52 57	oveq12d	⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) )
59	46 51 58	3eqtrd	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) )
60	45	oveq2d	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( i · ( ℑ ‘ 𝐶 ) ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
61	44 47 50	adddid	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
62	53 34 47	mulassd	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ( i · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) ) )
63	34 10 15 27 10	itgmulc2lem2	⊢ ( 𝜑 → ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 )
64	63	oveq2d	⊢ ( 𝜑 → ( i · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
65	62 64	eqtrd	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
66	53 34 53 48	mul4d	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
67		ixi	⊢ ( i · i ) = - 1
68	67	oveq1i	⊢ ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( - 1 · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
69	34 48	mulcld	⊢ ( 𝜑 → ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
70	69	mulm1d	⊢ ( 𝜑 → ( - 1 · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
71	68 70	eqtrid	⊢ ( 𝜑 → ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
72	34 48	mulneg1d	⊢ ( 𝜑 → ( - ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
73	29 19 22 28 19	itgmulc2lem2	⊢ ( 𝜑 → ( - ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
74	72 73	eqtr3d	⊢ ( 𝜑 → - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
75	66 71 74	3eqtrd	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
76	65 75	oveq12d	⊢ ( 𝜑 → ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
77	40 33 76	comraddd	⊢ ( 𝜑 → ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
78	60 61 77	3eqtrd	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
79	59 78	oveq12d	⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
80	5 42 44 79	joinlmuladdmuld	⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
81	35 20	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
82	12 81	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
83	35 20	mulneg1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) = - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) )
84	83	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
85	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
86	85 9	remuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
87	82 84 86	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ℜ ‘ ( 𝐶 · 𝐵 ) ) )
88	87	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) d 𝑥 = ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 )
89	12 16 31 32	itgadd	⊢ ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
90	88 89	eqtr3d	⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
91	85 9	immuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
92	91	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) d 𝑥 )
93	21 23 36 37	itgadd	⊢ ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
94	92 93	eqtrd	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
95	94	oveq2d	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) = ( i · ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
96	53 24 38	adddid	⊢ ( 𝜑 → ( i · ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) = ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
97	95 96	eqtrd	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) = ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
98	90 97	oveq12d	⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
99	41 80 98	3eqtr4d	⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) )
100	1	replimd	⊢ ( 𝜑 → 𝐶 = ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) )
101	100	oveq1d	⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) )
102	85 9	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
103	1 2 3	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )
104	102 103	itgcnval	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) )
105	99 101 104	3eqtr4d	⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )