Step | Hyp | Ref
| Expression |
1 | | mulcl 9899 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
2 | | eqidd 2611 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))) |
3 | | cosf 14694 |
. . . . . . . 8
⊢
cos:ℂ⟶ℂ |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
cos:ℂ⟶ℂ) |
5 | 4 | feqmptd 6159 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → cos =
(𝑦 ∈ ℂ ↦
(cos‘𝑦))) |
6 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = (𝐴 · 𝑥) → (cos‘𝑦) = (cos‘(𝐴 · 𝑥))) |
7 | 1, 2, 5, 6 | fmptco 6303 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (cos
∘ (𝑥 ∈ ℂ
↦ (𝐴 · 𝑥))) = (𝑥 ∈ ℂ ↦ (cos‘(𝐴 · 𝑥)))) |
8 | 7 | eqcomd 2616 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥))) = (cos ∘ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) |
9 | 8 | oveq2d 6565 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥)))) = (ℂ D (cos
∘ (𝑥 ∈ ℂ
↦ (𝐴 · 𝑥))))) |
10 | | cnelprrecn 9908 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
12 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) |
13 | 1, 12 | fmptd 6292 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)):ℂ⟶ℂ) |
14 | | dvcos 23550 |
. . . . . . 7
⊢ (ℂ
D cos) = (𝑥 ∈ ℂ
↦ -(sin‘𝑥)) |
15 | 14 | dmeqi 5247 |
. . . . . 6
⊢ dom
(ℂ D cos) = dom (𝑥
∈ ℂ ↦ -(sin‘𝑥)) |
16 | | dmmptg 5549 |
. . . . . . 7
⊢
(∀𝑥 ∈
ℂ -(sin‘𝑥)
∈ ℂ → dom (𝑥 ∈ ℂ ↦ -(sin‘𝑥)) = ℂ) |
17 | | sincl 14695 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
18 | 17 | negcld 10258 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
-(sin‘𝑥) ∈
ℂ) |
19 | 16, 18 | mprg 2910 |
. . . . . 6
⊢ dom
(𝑥 ∈ ℂ ↦
-(sin‘𝑥)) =
ℂ |
20 | 15, 19 | eqtri 2632 |
. . . . 5
⊢ dom
(ℂ D cos) = ℂ |
21 | 20 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D cos) = ℂ) |
22 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝐴 ∈
ℂ) |
23 | | 0red 9920 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 0 ∈
ℝ) |
24 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
25 | 11, 24 | dvmptc 23527 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
𝐴)) = (𝑥 ∈ ℂ ↦ 0)) |
26 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
27 | | 1red 9934 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 1 ∈
ℝ) |
28 | 11 | dvmptid 23526 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
𝑥)) = (𝑥 ∈ ℂ ↦ 1)) |
29 | 11, 22, 23, 25, 26, 27, 28 | dvmptmul 23530 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))) = (𝑥 ∈ ℂ ↦ ((0 · 𝑥) + (1 · 𝐴)))) |
30 | 29 | dmeqd 5248 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) = dom (𝑥 ∈ ℂ ↦ ((0
· 𝑥) + (1 ·
𝐴)))) |
31 | | dmmptg 5549 |
. . . . . 6
⊢
(∀𝑥 ∈
ℂ ((0 · 𝑥) +
(1 · 𝐴)) ∈ V
→ dom (𝑥 ∈
ℂ ↦ ((0 · 𝑥) + (1 · 𝐴))) = ℂ) |
32 | | ovex 6577 |
. . . . . . 7
⊢ ((0
· 𝑥) + (1 ·
𝐴)) ∈
V |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → ((0
· 𝑥) + (1 ·
𝐴)) ∈
V) |
34 | 31, 33 | mprg 2910 |
. . . . 5
⊢ dom
(𝑥 ∈ ℂ ↦
((0 · 𝑥) + (1
· 𝐴))) =
ℂ |
35 | 30, 34 | syl6eq 2660 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) =
ℂ) |
36 | 11, 11, 4, 13, 21, 35 | dvcof 23517 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (cos ∘ (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥)))) = (((ℂ D cos)
∘ (𝑥 ∈ ℂ
↦ (𝐴 · 𝑥))) ∘𝑓
· (ℂ D (𝑥
∈ ℂ ↦ (𝐴
· 𝑥))))) |
37 | | dvcos 23550 |
. . . . . . 7
⊢ (ℂ
D cos) = (𝑦 ∈ ℂ
↦ -(sin‘𝑦)) |
38 | 37 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D cos) = (𝑦 ∈ ℂ
↦ -(sin‘𝑦))) |
39 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = (𝐴 · 𝑥) → (sin‘𝑦) = (sin‘(𝐴 · 𝑥))) |
40 | 39 | negeqd 10154 |
. . . . . 6
⊢ (𝑦 = (𝐴 · 𝑥) → -(sin‘𝑦) = -(sin‘(𝐴 · 𝑥))) |
41 | 1, 2, 38, 40 | fmptco 6303 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
D cos) ∘ (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))) |
42 | 41 | oveq1d 6564 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(((ℂ D cos) ∘ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))) ∘𝑓 ·
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥)))) = ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))
∘𝑓 · (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) |
43 | | cnex 9896 |
. . . . . . 7
⊢ ℂ
∈ V |
44 | 43 | mptex 6390 |
. . . . . 6
⊢ (𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∈
V |
45 | | ovex 6577 |
. . . . . 6
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))) ∈ V |
46 | | offval3 7053 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∈ V ∧
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) ∈ V) →
((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))
∘𝑓 · (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) = (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)))) |
47 | 44, 45, 46 | mp2an 704 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))
∘𝑓 · (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) = (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦))) |
48 | 47 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))
∘𝑓 · (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) = (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)))) |
49 | 1 | sincld 14699 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(sin‘(𝐴 ·
𝑥)) ∈
ℂ) |
50 | 49 | negcld 10258 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
-(sin‘(𝐴 ·
𝑥)) ∈
ℂ) |
51 | 50 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈ ℂ
-(sin‘(𝐴 ·
𝑥)) ∈
ℂ) |
52 | | dmmptg 5549 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℂ -(sin‘(𝐴
· 𝑥)) ∈ ℂ
→ dom (𝑥 ∈
ℂ ↦ -(sin‘(𝐴 · 𝑥))) = ℂ) |
53 | 51, 52 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) =
ℂ) |
54 | 53, 35 | ineq12d 3777 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (dom
(𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∩ dom (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥)))) = (ℂ ∩
ℂ)) |
55 | | inidm 3784 |
. . . . . 6
⊢ (ℂ
∩ ℂ) = ℂ |
56 | 54, 55 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (dom
(𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∩ dom (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥)))) = ℂ) |
57 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) |
58 | 56 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) = ℂ) |
59 | 57, 58 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → 𝑦 ∈ ℂ) |
60 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → (𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))) |
61 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (sin‘(𝐴 · 𝑥)) = (sin‘(𝐴 · 𝑦))) |
63 | 62 | negeqd 10154 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → -(sin‘(𝐴 · 𝑥)) = -(sin‘(𝐴 · 𝑦))) |
64 | 63 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 = 𝑦) → -(sin‘(𝐴 · 𝑥)) = -(sin‘(𝐴 · 𝑦))) |
65 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
66 | | negex 10158 |
. . . . . . . . . . 11
⊢
-(sin‘(𝐴
· 𝑦)) ∈
V |
67 | 66 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ →
-(sin‘(𝐴 ·
𝑦)) ∈
V) |
68 | 60, 64, 65, 67 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) = -(sin‘(𝐴 · 𝑦))) |
69 | 68 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) = -(sin‘(𝐴 · 𝑦))) |
70 | 29 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (ℂ
D (𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))) = (𝑥 ∈ ℂ ↦ ((0 · 𝑥) + (1 · 𝐴)))) |
71 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (0 · 𝑥) = (0 · 𝑦)) |
72 | 71 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((0 · 𝑥) + (1 · 𝐴)) = ((0 · 𝑦) + (1 · 𝐴))) |
73 | | mul02 10093 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (0
· 𝑦) =
0) |
74 | | mulid2 9917 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
75 | 73, 74 | oveqan12rd 6569 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = (0 + 𝐴)) |
76 | | addid2 10098 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (0 +
𝐴) = 𝐴) |
77 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 +
𝐴) = 𝐴) |
78 | 75, 77 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = 𝐴) |
79 | 72, 78 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 = 𝑦) → ((0 · 𝑥) + (1 · 𝐴)) = 𝐴) |
80 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
81 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
82 | 70, 79, 80, 81 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥)))‘𝑦) = 𝐴) |
83 | 69, 82 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)) = (-(sin‘(𝐴 · 𝑦)) · 𝐴)) |
84 | | mulcl 9899 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
85 | 84 | sincld 14699 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(sin‘(𝐴 ·
𝑦)) ∈
ℂ) |
86 | 85 | negcld 10258 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
-(sin‘(𝐴 ·
𝑦)) ∈
ℂ) |
87 | 86, 81 | mulcomd 9940 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(-(sin‘(𝐴 ·
𝑦)) · 𝐴) = (𝐴 · -(sin‘(𝐴 · 𝑦)))) |
88 | 83, 87 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)) = (𝐴 · -(sin‘(𝐴 · 𝑦)))) |
89 | 59, 88 | syldan 486 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)) = (𝐴 · -(sin‘(𝐴 · 𝑦)))) |
90 | 56, 89 | mpteq12dva 4662 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
91 | 42, 48, 90 | 3eqtrd 2648 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((ℂ D cos) ∘ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))) ∘𝑓 ·
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
92 | 9, 36, 91 | 3eqtrd 2648 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
93 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐴 · 𝑦) = (𝐴 · 𝑥)) |
94 | 93 | fveq2d 6107 |
. . . . 5
⊢ (𝑦 = 𝑥 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑥))) |
95 | 94 | negeqd 10154 |
. . . 4
⊢ (𝑦 = 𝑥 → -(sin‘(𝐴 · 𝑦)) = -(sin‘(𝐴 · 𝑥))) |
96 | 95 | oveq2d 6565 |
. . 3
⊢ (𝑦 = 𝑥 → (𝐴 · -(sin‘(𝐴 · 𝑦))) = (𝐴 · -(sin‘(𝐴 · 𝑥)))) |
97 | 96 | cbvmptv 4678 |
. 2
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦)))) = (𝑥 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑥)))) |
98 | 92, 97 | syl6eq 2660 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥)))) = (𝑥 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑥))))) |