This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 )