Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | 1 | recld 13978 |
. . . . . . . 8
⊢ (𝜑 → (ℜ‘𝐶) ∈
ℝ) |
3 | 2 | recnd 10106 |
. . . . . . 7
⊢ (𝜑 → (ℜ‘𝐶) ∈
ℂ) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℂ) |
5 | | itgmulc2nc.3 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
6 | | iblmbf 23579 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
8 | | itgmulc2nc.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
9 | 7, 8 | mbfmptcl 23449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 9 | recld 13978 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
11 | 10 | recnd 10106 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
12 | 4, 11 | mulcld 10098 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ) |
13 | 9 | iblcn 23610 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
14 | 5, 13 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
15 | 14 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
16 | | itgmulc2nc.m |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) |
17 | | ovexd 6720 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V) |
18 | 16, 17 | mbfdm2 23450 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ dom vol) |
19 | | fconstmpt 5197 |
. . . . . . . . 9
⊢ (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))) |
21 | | eqidd 2652 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) |
22 | 18, 4, 10, 20, 21 | offval2 6956 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵)))) |
23 | | iblmbf 23579 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 →
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn) |
24 | 15, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn) |
25 | | eqid 2651 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) |
26 | 11, 25 | fmptd 6425 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ) |
27 | 24, 2, 26 | mbfmulc2re 23460 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn) |
28 | 22, 27 | eqeltrrd 2731 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn) |
29 | 3, 10, 15, 28 | iblmulc2nc 33605 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈
𝐿1) |
30 | 12, 29 | itgcl 23595 |
. . . 4
⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) |
31 | | ax-icn 10033 |
. . . . 5
⊢ i ∈
ℂ |
32 | 9 | imcld 13979 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
33 | 32 | recnd 10106 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
34 | 4, 33 | mulcld 10098 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ) |
35 | 14 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
36 | | eqidd 2652 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) |
37 | 18, 4, 32, 20, 36 | offval2 6956 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵)))) |
38 | | iblmbf 23579 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 →
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn) |
39 | 35, 38 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn) |
40 | | eqid 2651 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) |
41 | 33, 40 | fmptd 6425 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ) |
42 | 39, 2, 41 | mbfmulc2re 23460 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn) |
43 | 37, 42 | eqeltrrd 2731 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn) |
44 | 3, 32, 35, 43 | iblmulc2nc 33605 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈
𝐿1) |
45 | 34, 44 | itgcl 23595 |
. . . . 5
⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) |
46 | | mulcl 10058 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i ·
∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ) |
47 | 31, 45, 46 | sylancr 696 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ) |
48 | 1 | imcld 13979 |
. . . . . . . . 9
⊢ (𝜑 → (ℑ‘𝐶) ∈
ℝ) |
49 | 48 | recnd 10106 |
. . . . . . . 8
⊢ (𝜑 → (ℑ‘𝐶) ∈
ℂ) |
50 | 49 | negcld 10417 |
. . . . . . 7
⊢ (𝜑 → -(ℑ‘𝐶) ∈
ℂ) |
51 | 50 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐶) ∈ ℂ) |
52 | 51, 33 | mulcld 10098 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ) |
53 | | fconstmpt 5197 |
. . . . . . . . 9
⊢ (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶)) |
54 | 53 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶))) |
55 | 18, 51, 32, 54, 36 | offval2 6956 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵)))) |
56 | 48 | renegcld 10495 |
. . . . . . . 8
⊢ (𝜑 → -(ℑ‘𝐶) ∈
ℝ) |
57 | 39, 56, 41 | mbfmulc2re 23460 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn) |
58 | 55, 57 | eqeltrrd 2731 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn) |
59 | 50, 32, 35, 58 | iblmulc2nc 33605 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈
𝐿1) |
60 | 52, 59 | itgcl 23595 |
. . . 4
⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) |
61 | 49 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℂ) |
62 | 61, 11 | mulcld 10098 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ) |
63 | | fconstmpt 5197 |
. . . . . . . . . 10
⊢ (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) |
64 | 63 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))) |
65 | 18, 61, 10, 64, 21 | offval2 6956 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵)))) |
66 | 24, 48, 26 | mbfmulc2re 23460 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn) |
67 | 65, 66 | eqeltrrd 2731 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn) |
68 | 49, 10, 15, 67 | iblmulc2nc 33605 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈
𝐿1) |
69 | 62, 68 | itgcl 23595 |
. . . . 5
⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) |
70 | | mulcl 10058 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i ·
∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ) |
71 | 31, 69, 70 | sylancr 696 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ) |
72 | 30, 47, 60, 71 | add4d 10302 |
. . 3
⊢ (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
73 | 31 | a1i 11 |
. . . . . 6
⊢ (𝜑 → i ∈
ℂ) |
74 | 73, 49 | mulcld 10098 |
. . . . 5
⊢ (𝜑 → (i ·
(ℑ‘𝐶)) ∈
ℂ) |
75 | 8, 5 | itgcl 23595 |
. . . . 5
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ) |
76 | 3, 74, 75 | adddird 10103 |
. . . 4
⊢ (𝜑 → (((ℜ‘𝐶) + (i ·
(ℑ‘𝐶)))
· ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥))) |
77 | 8, 5 | itgcnval 23611 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) |
78 | 77 | oveq2d 6706 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))) |
79 | 10, 15 | itgcl 23595 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ) |
80 | 32, 35 | itgcl 23595 |
. . . . . . . 8
⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) |
81 | | mulcl 10058 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i ·
∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
82 | 31, 80, 81 | sylancr 696 |
. . . . . . 7
⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
83 | 3, 79, 82 | adddid 10102 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)))) |
84 | 3, 10, 15, 28, 2, 10 | itgmulc2nclem2 33607 |
. . . . . . 7
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥) |
85 | 3, 73, 80 | mul12d 10283 |
. . . . . . . 8
⊢ (𝜑 → ((ℜ‘𝐶) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))) |
86 | 3, 32, 35, 43, 2, 32 | itgmulc2nclem2 33607 |
. . . . . . . . 9
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
87 | 86 | oveq2d 6706 |
. . . . . . . 8
⊢ (𝜑 → (i ·
((ℜ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
88 | 85, 87 | eqtrd 2685 |
. . . . . . 7
⊢ (𝜑 → ((ℜ‘𝐶) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
89 | 84, 88 | oveq12d 6708 |
. . . . . 6
⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))) |
90 | 78, 83, 89 | 3eqtrd 2689 |
. . . . 5
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))) |
91 | 77 | oveq2d 6706 |
. . . . . 6
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))) |
92 | 74, 79, 82 | adddid 10102 |
. . . . . 6
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
(∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥)))) |
93 | 73, 49, 79 | mulassd 10101 |
. . . . . . . . 9
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥))) |
94 | 49, 10, 15, 67, 48, 10 | itgmulc2nclem2 33607 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) |
95 | 94 | oveq2d 6706 |
. . . . . . . . 9
⊢ (𝜑 → (i ·
((ℑ‘𝐶) ·
∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
96 | 93, 95 | eqtrd 2685 |
. . . . . . . 8
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
97 | 73, 49, 73, 80 | mul4d 10286 |
. . . . . . . . 9
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
(i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) ·
((ℑ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥))) |
98 | | ixi 10694 |
. . . . . . . . . . 11
⊢ (i
· i) = -1 |
99 | 98 | oveq1i 6700 |
. . . . . . . . . 10
⊢ ((i
· i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
100 | 49, 80 | mulcld 10098 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
101 | 100 | mulm1d 10520 |
. . . . . . . . . 10
⊢ (𝜑 → (-1 ·
((ℑ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
102 | 99, 101 | syl5eq 2697 |
. . . . . . . . 9
⊢ (𝜑 → ((i · i) ·
((ℑ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
103 | 49, 80 | mulneg1d 10521 |
. . . . . . . . . 10
⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
104 | 50, 32, 35, 58, 56, 32 | itgmulc2nclem2 33607 |
. . . . . . . . . 10
⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
105 | 103, 104 | eqtr3d 2687 |
. . . . . . . . 9
⊢ (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
106 | 97, 102, 105 | 3eqtrd 2689 |
. . . . . . . 8
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
(i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
107 | 96, 106 | oveq12d 6708 |
. . . . . . 7
⊢ (𝜑 → (((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
108 | 71, 60 | addcomd 10276 |
. . . . . . 7
⊢ (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
109 | 107, 108 | eqtrd 2685 |
. . . . . 6
⊢ (𝜑 → (((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
110 | 91, 92, 109 | 3eqtrd 2689 |
. . . . 5
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
111 | 90, 110 | oveq12d 6708 |
. . . 4
⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
112 | 76, 111 | eqtrd 2685 |
. . 3
⊢ (𝜑 → (((ℜ‘𝐶) + (i ·
(ℑ‘𝐶)))
· ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
113 | 61, 33 | mulcld 10098 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ) |
114 | 18, 61, 32, 64, 36 | offval2 6956 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵)))) |
115 | 39, 48, 41 | mbfmulc2re 23460 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn) |
116 | 114, 115 | eqeltrrd 2731 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn) |
117 | 49, 32, 35, 116 | iblmulc2nc 33605 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈
𝐿1) |
118 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
119 | 118, 9 | mulcld 10098 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) |
120 | | eqidd 2652 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) |
121 | | ref 13896 |
. . . . . . . . . . 11
⊢
ℜ:ℂ⟶ℝ |
122 | 121 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
ℜ:ℂ⟶ℝ) |
123 | 122 | feqmptd 6288 |
. . . . . . . . 9
⊢ (𝜑 → ℜ = (𝑘 ∈ ℂ ↦
(ℜ‘𝑘))) |
124 | | fveq2 6229 |
. . . . . . . . 9
⊢ (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵))) |
125 | 119, 120,
123, 124 | fmptco 6436 |
. . . . . . . 8
⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵)))) |
126 | 118, 9 | remuld 14002 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) |
127 | 126 | mpteq2dva 4777 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))) |
128 | 125, 127 | eqtrd 2685 |
. . . . . . 7
⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))) |
129 | | eqid 2651 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) |
130 | 119, 129 | fmptd 6425 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ) |
131 | | ismbfcn 23443 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))) |
132 | 130, 131 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))) |
133 | 16, 132 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)) |
134 | 133 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn) |
135 | 128, 134 | eqeltrrd 2731 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn) |
136 | 12, 29, 113, 117, 135 | itgsubnc 33602 |
. . . . 5
⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
137 | 126 | itgeq2dv 23593 |
. . . . 5
⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥) |
138 | 113, 117 | itgneg 23615 |
. . . . . . . 8
⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
139 | 61, 33 | mulneg1d 10521 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵))) |
140 | 139 | itgeq2dv 23593 |
. . . . . . . 8
⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
141 | 138, 140 | eqtr4d 2688 |
. . . . . . 7
⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
142 | 141 | oveq2d 6706 |
. . . . . 6
⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
143 | 113, 117 | itgcl 23595 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) |
144 | 30, 143 | negsubd 10436 |
. . . . . 6
⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
145 | 142, 144 | eqtr3d 2687 |
. . . . 5
⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
146 | 136, 137,
145 | 3eqtr4d 2695 |
. . . 4
⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
147 | 118, 9 | immuld 14003 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) |
148 | 147 | itgeq2dv 23593 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥) |
149 | | imf 13897 |
. . . . . . . . . . . . 13
⊢
ℑ:ℂ⟶ℝ |
150 | 149 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 →
ℑ:ℂ⟶ℝ) |
151 | 150 | feqmptd 6288 |
. . . . . . . . . . 11
⊢ (𝜑 → ℑ = (𝑘 ∈ ℂ ↦
(ℑ‘𝑘))) |
152 | | fveq2 6229 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵))) |
153 | 119, 120,
151, 152 | fmptco 6436 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵)))) |
154 | 147 | mpteq2dva 4777 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))) |
155 | 153, 154 | eqtrd 2685 |
. . . . . . . . 9
⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))) |
156 | 133 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn) |
157 | 155, 156 | eqeltrrd 2731 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn) |
158 | 34, 44, 62, 68, 157 | itgaddnc 33600 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
159 | 148, 158 | eqtrd 2685 |
. . . . . 6
⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
160 | 159 | oveq2d 6706 |
. . . . 5
⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
161 | 73, 45, 69 | adddid 10102 |
. . . . 5
⊢ (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
162 | 160, 161 | eqtrd 2685 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
163 | 146, 162 | oveq12d 6708 |
. . 3
⊢ (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
164 | 72, 112, 163 | 3eqtr4d 2695 |
. 2
⊢ (𝜑 → (((ℜ‘𝐶) + (i ·
(ℑ‘𝐶)))
· ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥))) |
165 | 1 | replimd 13981 |
. . 3
⊢ (𝜑 → 𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶)))) |
166 | 165 | oveq1d 6705 |
. 2
⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥)) |
167 | 1, 8, 5, 16 | iblmulc2nc 33605 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈
𝐿1) |
168 | 119, 167 | itgcnval 23611 |
. 2
⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥))) |
169 | 164, 166,
168 | 3eqtr4d 2695 |
1
⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) |