Metamath Proof Explorer

Theorem itgmulc2nc

Description: Choice-free analogue of itgmulc2 . (Contributed by Brendan Leahy, 19-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 itgmulc2nc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 itgmulc2nc.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4 itgmulc2nc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
5 1 recld ⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℂ )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
8 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
9 3 8 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
10 9 2 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
11 10 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
13 7 12 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
14 10 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
15 3 14 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
16 15 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
17 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ V )
18 4 17 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
19 fconstmpt ⊢ ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) )
20 19 a1i ⊢ ( 𝜑 → ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) )
21 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) )
22 18 7 11 20 21 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
23 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
24 16 23 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
25 12 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
26 24 5 25 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
27 22 26 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
28 6 11 16 27 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
29 13 28 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
30 ax-icn ⊢ i ∈ ℂ
31 10 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
32 31 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
33 7 32 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
34 15 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
35 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) )
36 18 7 31 20 35 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
37 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
38 34 37 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
39 32 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
40 38 5 39 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
41 36 40 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
42 6 31 34 41 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
43 33 42 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
44 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
45 30 43 44 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
46 1 imcld ⊢ ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℝ )
47 46 recnd ⊢ ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℂ )
48 47 negcld ⊢ ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℂ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℂ )
50 49 32 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
51 fconstmpt ⊢ ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) )
52 51 a1i ⊢ ( 𝜑 → ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) ) )
53 18 49 31 52 35 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
54 46 renegcld ⊢ ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
55 38 54 39 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
56 53 55 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
57 48 31 34 56 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
58 50 57 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
59 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
60 59 12 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
61 fconstmpt ⊢ ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) )
62 61 a1i ⊢ ( 𝜑 → ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) )
63 18 59 11 62 21 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
64 24 46 25 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
65 63 64 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
66 47 11 16 65 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
67 60 66 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
68 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
69 30 67 68 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
70 29 45 58 69 add4d ⊢ ( 𝜑 → ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
71 30 a1i ⊢ ( 𝜑 → i ∈ ℂ )
72 71 47 mulcld ⊢ ( 𝜑 → ( i · ( ℑ ‘ 𝐶 ) ) ∈ ℂ )
73 2 3 itgcl ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
74 6 72 73 adddird ⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) ) )
75 2 3 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
76 75 oveq2d ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ℜ ‘ 𝐶 ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
77 11 16 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
78 31 34 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
79 mulcl ⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
80 30 78 79 sylancr ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
81 6 77 80 adddid ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
82 6 11 16 27 5 11 itgmulc2nclem2 ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 )
83 6 71 78 mul12d ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
84 6 31 34 41 5 31 itgmulc2nclem2 ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
85 84 oveq2d ⊢ ( 𝜑 → ( i · ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
86 83 85 eqtrd ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
87 82 86 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) )
88 76 81 87 3eqtrd ⊢ ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) )
89 75 oveq2d ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( i · ( ℑ ‘ 𝐶 ) ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
90 72 77 80 adddid ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
91 71 47 77 mulassd ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ( i · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) ) )
92 47 11 16 65 46 11 itgmulc2nclem2 ⊢ ( 𝜑 → ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 )
93 92 oveq2d ⊢ ( 𝜑 → ( i · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
94 91 93 eqtrd ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
95 71 47 71 78 mul4d ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
96 ixi ⊢ ( i · i ) = - 1
97 96 oveq1i ⊢ ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( - 1 · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
98 47 78 mulcld ⊢ ( 𝜑 → ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
99 98 mulm1d ⊢ ( 𝜑 → ( - 1 · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
100 97 99 eqtrid ⊢ ( 𝜑 → ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
101 47 78 mulneg1d ⊢ ( 𝜑 → ( - ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
102 48 31 34 56 54 31 itgmulc2nclem2 ⊢ ( 𝜑 → ( - ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
103 101 102 eqtr3d ⊢ ( 𝜑 → - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
104 95 100 103 3eqtrd ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
105 94 104 oveq12d ⊢ ( 𝜑 → ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
106 69 58 addcomd ⊢ ( 𝜑 → ( ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
107 105 106 eqtrd ⊢ ( 𝜑 → ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
108 89 90 107 3eqtrd ⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
109 88 108 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
110 74 109 eqtrd ⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
111 59 32 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
112 18 59 31 62 35 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
113 38 46 39 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
114 112 113 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
115 47 31 34 114 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
116 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
117 116 10 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
118 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) )
119 ref ⊢ ℜ : ℂ ⟶ ℝ
120 119 a1i ⊢ ( 𝜑 → ℜ : ℂ ⟶ ℝ )
121 120 feqmptd ⊢ ( 𝜑 → ℜ = ( 𝑘 ∈ ℂ ↦ ( ℜ ‘ 𝑘 ) ) )
122 fveq2 ⊢ ( 𝑘 = ( 𝐶 · 𝐵 ) → ( ℜ ‘ 𝑘 ) = ( ℜ ‘ ( 𝐶 · 𝐵 ) ) )
123 117 118 121 122 fmptco ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) )
124 116 10 remuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
125 124 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
126 123 125 eqtrd ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
127 117 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ )
128 ismbfcn ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) ) )
129 127 128 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) ) )
130 4 129 mpbid ⊢ ( 𝜑 → ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) )
131 130 simpld ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
132 126 131 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) ∈ MblFn )
133 13 28 111 115 132 itgsubnc ⊢ ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 − ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
134 124 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) d 𝑥 )
135 111 115 itgneg ⊢ ( 𝜑 → - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 = ∫ 𝐴 - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
136 59 32 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) = - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) )
137 136 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 = ∫ 𝐴 - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
138 135 137 eqtr4d ⊢ ( 𝜑 → - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
139 138 oveq2d ⊢ ( 𝜑 → ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
140 111 115 itgcl ⊢ ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
141 29 140 negsubd ⊢ ( 𝜑 → ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 − ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
142 139 141 eqtr3d ⊢ ( 𝜑 → ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 − ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
143 133 134 142 3eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
144 116 10 immuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
145 144 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) d 𝑥 )
146 imf ⊢ ℑ : ℂ ⟶ ℝ
147 146 a1i ⊢ ( 𝜑 → ℑ : ℂ ⟶ ℝ )
148 147 feqmptd ⊢ ( 𝜑 → ℑ = ( 𝑘 ∈ ℂ ↦ ( ℑ ‘ 𝑘 ) ) )
149 fveq2 ⊢ ( 𝑘 = ( 𝐶 · 𝐵 ) → ( ℑ ‘ 𝑘 ) = ( ℑ ‘ ( 𝐶 · 𝐵 ) ) )
150 117 118 148 149 fmptco ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) )
151 144 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
152 150 151 eqtrd ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
153 130 simprd ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
154 152 153 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) ∈ MblFn )
155 33 42 60 66 154 itgaddnc ⊢ ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
156 145 155 eqtrd ⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
157 156 oveq2d ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) = ( i · ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
158 71 43 67 adddid ⊢ ( 𝜑 → ( i · ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) = ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
159 157 158 eqtrd ⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) = ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
160 143 159 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
161 70 110 160 3eqtr4d ⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) )
162 1 replimd ⊢ ( 𝜑 → 𝐶 = ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) )
163 162 oveq1d ⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) )
164 1 2 3 4 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )
165 117 164 itgcnval ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) )
166 161 163 165 3eqtr4d ⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )