Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | 1 | recld 13782 |
. . . . . . . 8
⊢ (𝜑 → (ℜ‘𝐶) ∈
ℝ) |
3 | 2 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (ℜ‘𝐶) ∈
ℂ) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℂ) |
5 | | itgmulc2nc.3 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
6 | | iblmbf 23340 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
8 | | itgmulc2nc.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
9 | 7, 8 | mbfmptcl 23210 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 9 | recld 13782 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
11 | 10 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
12 | 4, 11 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ) |
13 | 9 | iblcn 23371 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
14 | 5, 13 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
15 | 14 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
16 | | itgmulc2nc.m |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) |
17 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐶 · 𝐵) ∈ V |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V) |
19 | 16, 18 | mbfdm2 23211 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ dom vol) |
20 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))) |
22 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) |
23 | 19, 4, 10, 21, 22 | offval2 6812 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵)))) |
24 | | iblmbf 23340 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 →
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn) |
25 | 15, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn) |
26 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) |
27 | 11, 26 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ) |
28 | 25, 2, 27 | mbfmulc2re 23221 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn) |
29 | 23, 28 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn) |
30 | 3, 10, 15, 29 | iblmulc2nc 32645 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈
𝐿1) |
31 | 12, 30 | itgcl 23356 |
. . . 4
⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) |
32 | | ax-icn 9874 |
. . . . 5
⊢ i ∈
ℂ |
33 | 9 | imcld 13783 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
34 | 33 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
35 | 4, 34 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ) |
36 | 14 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
37 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) |
38 | 19, 4, 33, 21, 37 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵)))) |
39 | | iblmbf 23340 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 →
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn) |
40 | 36, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn) |
41 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) |
42 | 34, 41 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ) |
43 | 40, 2, 42 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn) |
44 | 38, 43 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn) |
45 | 3, 33, 36, 44 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈
𝐿1) |
46 | 35, 45 | itgcl 23356 |
. . . . 5
⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) |
47 | | mulcl 9899 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i ·
∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ) |
48 | 32, 46, 47 | sylancr 694 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ) |
49 | 1 | imcld 13783 |
. . . . . . . . 9
⊢ (𝜑 → (ℑ‘𝐶) ∈
ℝ) |
50 | 49 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (ℑ‘𝐶) ∈
ℂ) |
51 | 50 | negcld 10258 |
. . . . . . 7
⊢ (𝜑 → -(ℑ‘𝐶) ∈
ℂ) |
52 | 51 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐶) ∈ ℂ) |
53 | 52, 34 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ) |
54 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶)) |
55 | 54 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶))) |
56 | 19, 52, 33, 55, 37 | offval2 6812 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵)))) |
57 | 49 | renegcld 10336 |
. . . . . . . 8
⊢ (𝜑 → -(ℑ‘𝐶) ∈
ℝ) |
58 | 40, 57, 42 | mbfmulc2re 23221 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn) |
59 | 56, 58 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn) |
60 | 51, 33, 36, 59 | iblmulc2nc 32645 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈
𝐿1) |
61 | 53, 60 | itgcl 23356 |
. . . 4
⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) |
62 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℂ) |
63 | 62, 11 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ) |
64 | | fconstmpt 5085 |
. . . . . . . . . 10
⊢ (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) |
65 | 64 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))) |
66 | 19, 62, 10, 65, 22 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵)))) |
67 | 25, 49, 27 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn) |
68 | 66, 67 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn) |
69 | 50, 10, 15, 68 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈
𝐿1) |
70 | 63, 69 | itgcl 23356 |
. . . . 5
⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) |
71 | | mulcl 9899 |
. . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i ·
∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ) |
72 | 32, 70, 71 | sylancr 694 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ) |
73 | 31, 48, 61, 72 | add4d 10143 |
. . 3
⊢ (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
74 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → i ∈
ℂ) |
75 | 74, 50 | mulcld 9939 |
. . . . 5
⊢ (𝜑 → (i ·
(ℑ‘𝐶)) ∈
ℂ) |
76 | 8, 5 | itgcl 23356 |
. . . . 5
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ) |
77 | 3, 75, 76 | adddird 9944 |
. . . 4
⊢ (𝜑 → (((ℜ‘𝐶) + (i ·
(ℑ‘𝐶)))
· ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥))) |
78 | 8, 5 | itgcnval 23372 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) |
79 | 78 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))) |
80 | 10, 15 | itgcl 23356 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ) |
81 | 33, 36 | itgcl 23356 |
. . . . . . . 8
⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) |
82 | | mulcl 9899 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i ·
∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
83 | 32, 81, 82 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
84 | 3, 80, 83 | adddid 9943 |
. . . . . 6
⊢ (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)))) |
85 | 3, 10, 15, 29, 2, 10 | itgmulc2nclem2 32647 |
. . . . . . 7
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥) |
86 | 3, 74, 81 | mul12d 10124 |
. . . . . . . 8
⊢ (𝜑 → ((ℜ‘𝐶) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))) |
87 | 3, 33, 36, 44, 2, 33 | itgmulc2nclem2 32647 |
. . . . . . . . 9
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
88 | 87 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (i ·
((ℜ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
89 | 86, 88 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((ℜ‘𝐶) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
90 | 85, 89 | oveq12d 6567 |
. . . . . 6
⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))) |
91 | 79, 84, 90 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))) |
92 | 78 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))) |
93 | 75, 80, 83 | adddid 9943 |
. . . . . 6
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
(∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥)))) |
94 | 74, 50, 80 | mulassd 9942 |
. . . . . . . . 9
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥))) |
95 | 50, 10, 15, 68, 49, 10 | itgmulc2nclem2 32647 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) |
96 | 95 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (i ·
((ℑ‘𝐶) ·
∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
97 | 94, 96 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
98 | 74, 50, 74, 81 | mul4d 10127 |
. . . . . . . . 9
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
(i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) ·
((ℑ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥))) |
99 | | ixi 10535 |
. . . . . . . . . . 11
⊢ (i
· i) = -1 |
100 | 99 | oveq1i 6559 |
. . . . . . . . . 10
⊢ ((i
· i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
101 | 50, 81 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) |
102 | 101 | mulm1d 10361 |
. . . . . . . . . 10
⊢ (𝜑 → (-1 ·
((ℑ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
103 | 100, 102 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((i · i) ·
((ℑ‘𝐶) ·
∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
104 | 50, 81 | mulneg1d 10362 |
. . . . . . . . . 10
⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) |
105 | 51, 33, 36, 59, 57, 33 | itgmulc2nclem2 32647 |
. . . . . . . . . 10
⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
106 | 104, 105 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
107 | 98, 103, 106 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
(i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
108 | 97, 107 | oveq12d 6567 |
. . . . . . 7
⊢ (𝜑 → (((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
109 | 72, 61 | addcomd 10117 |
. . . . . . 7
⊢ (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
110 | 108, 109 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (((i ·
(ℑ‘𝐶)) ·
∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i ·
∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
111 | 92, 93, 110 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → ((i ·
(ℑ‘𝐶)) ·
∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
112 | 91, 111 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
113 | 77, 112 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (((ℜ‘𝐶) + (i ·
(ℑ‘𝐶)))
· ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
114 | 62, 34 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ) |
115 | 19, 62, 33, 65, 37 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵)))) |
116 | 40, 49, 42 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn) |
117 | 115, 116 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn) |
118 | 50, 33, 36, 117 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈
𝐿1) |
119 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
120 | 119, 9 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) |
121 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) |
122 | | ref 13700 |
. . . . . . . . . . 11
⊢
ℜ:ℂ⟶ℝ |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 →
ℜ:ℂ⟶ℝ) |
124 | 123 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → ℜ = (𝑘 ∈ ℂ ↦
(ℜ‘𝑘))) |
125 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵))) |
126 | 120, 121,
124, 125 | fmptco 6303 |
. . . . . . . 8
⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵)))) |
127 | 119, 9 | remuld 13806 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) |
128 | 127 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))) |
129 | 126, 128 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))) |
130 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) |
131 | 120, 130 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ) |
132 | | ismbfcn 23204 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))) |
133 | 131, 132 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))) |
134 | 16, 133 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘
(𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)) |
135 | 134 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn) |
136 | 129, 135 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn) |
137 | 12, 30, 114, 118, 136 | itgsubnc 32642 |
. . . . 5
⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
138 | 127 | itgeq2dv 23354 |
. . . . 5
⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥) |
139 | 114, 118 | itgneg 23376 |
. . . . . . . 8
⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
140 | 62, 34 | mulneg1d 10362 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵))) |
141 | 140 | itgeq2dv 23354 |
. . . . . . . 8
⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
142 | 139, 141 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) |
143 | 142 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
144 | 114, 118 | itgcl 23356 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) |
145 | 31, 144 | negsubd 10277 |
. . . . . 6
⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
146 | 143, 145 | eqtr3d 2646 |
. . . . 5
⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
147 | 137, 138,
146 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)) |
148 | 119, 9 | immuld 13807 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) |
149 | 148 | itgeq2dv 23354 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥) |
150 | | imf 13701 |
. . . . . . . . . . . . 13
⊢
ℑ:ℂ⟶ℝ |
151 | 150 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 →
ℑ:ℂ⟶ℝ) |
152 | 151 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → ℑ = (𝑘 ∈ ℂ ↦
(ℑ‘𝑘))) |
153 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵))) |
154 | 120, 121,
152, 153 | fmptco 6303 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵)))) |
155 | 148 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))) |
156 | 154, 155 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))) |
157 | 134 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn) |
158 | 156, 157 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn) |
159 | 35, 45, 63, 69, 158 | itgaddnc 32640 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
160 | 149, 159 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) |
161 | 160 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
162 | 74, 46, 70 | adddid 9943 |
. . . . 5
⊢ (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
163 | 161, 162 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) |
164 | 147, 163 | oveq12d 6567 |
. . 3
⊢ (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))) |
165 | 73, 113, 164 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → (((ℜ‘𝐶) + (i ·
(ℑ‘𝐶)))
· ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥))) |
166 | 1 | replimd 13785 |
. . 3
⊢ (𝜑 → 𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶)))) |
167 | 166 | oveq1d 6564 |
. 2
⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥)) |
168 | 1, 8, 5, 16 | iblmulc2nc 32645 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈
𝐿1) |
169 | 120, 168 | itgcnval 23372 |
. 2
⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥))) |
170 | 165, 167,
169 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) |