| Step | Hyp | Ref
| Expression |
| 1 | | mulcl 11239 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
| 2 | | eqidd 2738 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))) |
| 3 | | cosf 16161 |
. . . . . . . 8
⊢
cos:ℂ⟶ℂ |
| 4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
cos:ℂ⟶ℂ) |
| 5 | 4 | feqmptd 6977 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → cos =
(𝑦 ∈ ℂ ↦
(cos‘𝑦))) |
| 6 | | fveq2 6906 |
. . . . . 6
⊢ (𝑦 = (𝐴 · 𝑥) → (cos‘𝑦) = (cos‘(𝐴 · 𝑥))) |
| 7 | 1, 2, 5, 6 | fmptco 7149 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (cos
∘ (𝑥 ∈ ℂ
↦ (𝐴 · 𝑥))) = (𝑥 ∈ ℂ ↦ (cos‘(𝐴 · 𝑥)))) |
| 8 | 7 | eqcomd 2743 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥))) = (cos ∘ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) |
| 9 | 8 | oveq2d 7447 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥)))) = (ℂ D (cos
∘ (𝑥 ∈ ℂ
↦ (𝐴 · 𝑥))))) |
| 10 | | cnelprrecn 11248 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
| 11 | 10 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) |
| 12 | 1 | fmpttd 7135 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)):ℂ⟶ℂ) |
| 13 | | dvcos 26021 |
. . . . . . 7
⊢ (ℂ
D cos) = (𝑥 ∈ ℂ
↦ -(sin‘𝑥)) |
| 14 | 13 | dmeqi 5915 |
. . . . . 6
⊢ dom
(ℂ D cos) = dom (𝑥
∈ ℂ ↦ -(sin‘𝑥)) |
| 15 | | dmmptg 6262 |
. . . . . . 7
⊢
(∀𝑥 ∈
ℂ -(sin‘𝑥)
∈ ℂ → dom (𝑥 ∈ ℂ ↦ -(sin‘𝑥)) = ℂ) |
| 16 | | sincl 16162 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(sin‘𝑥) ∈
ℂ) |
| 17 | 16 | negcld 11607 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ →
-(sin‘𝑥) ∈
ℂ) |
| 18 | 15, 17 | mprg 3067 |
. . . . . 6
⊢ dom
(𝑥 ∈ ℂ ↦
-(sin‘𝑥)) =
ℂ |
| 19 | 14, 18 | eqtri 2765 |
. . . . 5
⊢ dom
(ℂ D cos) = ℂ |
| 20 | 19 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D cos) = ℂ) |
| 21 | | simpl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 22 | | 0red 11264 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 0 ∈
ℝ) |
| 23 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
| 24 | 11, 23 | dvmptc 25996 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
𝐴)) = (𝑥 ∈ ℂ ↦ 0)) |
| 25 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
| 26 | | 1red 11262 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → 1 ∈
ℝ) |
| 27 | 11 | dvmptid 25995 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
𝑥)) = (𝑥 ∈ ℂ ↦ 1)) |
| 28 | 11, 21, 22, 24, 25, 26, 27 | dvmptmul 25999 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))) = (𝑥 ∈ ℂ ↦ ((0 · 𝑥) + (1 · 𝐴)))) |
| 29 | 28 | dmeqd 5916 |
. . . . 5
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) = dom (𝑥 ∈ ℂ ↦ ((0
· 𝑥) + (1 ·
𝐴)))) |
| 30 | | dmmptg 6262 |
. . . . . 6
⊢
(∀𝑥 ∈
ℂ ((0 · 𝑥) +
(1 · 𝐴)) ∈ V
→ dom (𝑥 ∈
ℂ ↦ ((0 · 𝑥) + (1 · 𝐴))) = ℂ) |
| 31 | | ovex 7464 |
. . . . . . 7
⊢ ((0
· 𝑥) + (1 ·
𝐴)) ∈
V |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → ((0
· 𝑥) + (1 ·
𝐴)) ∈
V) |
| 33 | 30, 32 | mprg 3067 |
. . . . 5
⊢ dom
(𝑥 ∈ ℂ ↦
((0 · 𝑥) + (1
· 𝐴))) =
ℂ |
| 34 | 29, 33 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 ∈ ℂ → dom
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) =
ℂ) |
| 35 | 11, 11, 4, 12, 20, 34 | dvcof 25986 |
. . 3
⊢ (𝐴 ∈ ℂ → (ℂ
D (cos ∘ (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥)))) = (((ℂ D cos)
∘ (𝑥 ∈ ℂ
↦ (𝐴 · 𝑥))) ∘f ·
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))))) |
| 36 | | dvcos 26021 |
. . . . . . 7
⊢ (ℂ
D cos) = (𝑦 ∈ ℂ
↦ -(sin‘𝑦)) |
| 37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (ℂ
D cos) = (𝑦 ∈ ℂ
↦ -(sin‘𝑦))) |
| 38 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑦 = (𝐴 · 𝑥) → (sin‘𝑦) = (sin‘(𝐴 · 𝑥))) |
| 39 | 38 | negeqd 11502 |
. . . . . 6
⊢ (𝑦 = (𝐴 · 𝑥) → -(sin‘𝑦) = -(sin‘(𝐴 · 𝑥))) |
| 40 | 1, 2, 37, 39 | fmptco 7149 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((ℂ
D cos) ∘ (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))) |
| 41 | 40 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(((ℂ D cos) ∘ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))) ∘f · (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥)))) = ((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∘f · (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))))) |
| 42 | | cnex 11236 |
. . . . . . 7
⊢ ℂ
∈ V |
| 43 | 42 | mptex 7243 |
. . . . . 6
⊢ (𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∈
V |
| 44 | | ovex 7464 |
. . . . . 6
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))) ∈ V |
| 45 | | offval3 8007 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∈ V ∧
(ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥))) ∈ V) →
((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∘f
· (ℂ D (𝑥
∈ ℂ ↦ (𝐴
· 𝑥)))) = (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)))) |
| 46 | 43, 44, 45 | mp2an 692 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∘f
· (ℂ D (𝑥
∈ ℂ ↦ (𝐴
· 𝑥)))) = (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦))) |
| 47 | 46 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∘f
· (ℂ D (𝑥
∈ ℂ ↦ (𝐴
· 𝑥)))) = (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)))) |
| 48 | 1 | sincld 16166 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(sin‘(𝐴 ·
𝑥)) ∈
ℂ) |
| 49 | 48 | negcld 11607 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
-(sin‘(𝐴 ·
𝑥)) ∈
ℂ) |
| 50 | 49 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈ ℂ
-(sin‘(𝐴 ·
𝑥)) ∈
ℂ) |
| 51 | | dmmptg 6262 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ℂ -(sin‘(𝐴
· 𝑥)) ∈ ℂ
→ dom (𝑥 ∈
ℂ ↦ -(sin‘(𝐴 · 𝑥))) = ℂ) |
| 52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → dom
(𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) =
ℂ) |
| 53 | 52, 34 | ineq12d 4221 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (dom
(𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∩ dom (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥)))) = (ℂ ∩
ℂ)) |
| 54 | | inidm 4227 |
. . . . . 6
⊢ (ℂ
∩ ℂ) = ℂ |
| 55 | 53, 54 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (dom
(𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) ∩ dom (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥)))) = ℂ) |
| 56 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) |
| 57 | 55 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) = ℂ) |
| 58 | 56, 57 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → 𝑦 ∈ ℂ) |
| 59 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → (𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥))) = (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))) |
| 60 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
| 61 | 60 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (sin‘(𝐴 · 𝑥)) = (sin‘(𝐴 · 𝑦))) |
| 62 | 61 | negeqd 11502 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → -(sin‘(𝐴 · 𝑥)) = -(sin‘(𝐴 · 𝑦))) |
| 63 | 62 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 = 𝑦) → -(sin‘(𝐴 · 𝑥)) = -(sin‘(𝐴 · 𝑦))) |
| 64 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
| 65 | | negex 11506 |
. . . . . . . . . . 11
⊢
-(sin‘(𝐴
· 𝑦)) ∈
V |
| 66 | 65 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ →
-(sin‘(𝐴 ·
𝑦)) ∈
V) |
| 67 | 59, 63, 64, 66 | fvmptd 7023 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ → ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) = -(sin‘(𝐴 · 𝑦))) |
| 68 | 67 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) = -(sin‘(𝐴 · 𝑦))) |
| 69 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (ℂ
D (𝑥 ∈ ℂ ↦
(𝐴 · 𝑥))) = (𝑥 ∈ ℂ ↦ ((0 · 𝑥) + (1 · 𝐴)))) |
| 70 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (0 · 𝑥) = (0 · 𝑦)) |
| 71 | 70 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((0 · 𝑥) + (1 · 𝐴)) = ((0 · 𝑦) + (1 · 𝐴))) |
| 72 | | mul02 11439 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → (0
· 𝑦) =
0) |
| 73 | | mullid 11260 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 74 | 72, 73 | oveqan12rd 7451 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = (0 + 𝐴)) |
| 75 | | addlid 11444 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (0 +
𝐴) = 𝐴) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (0 +
𝐴) = 𝐴) |
| 77 | 74, 76 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0
· 𝑦) + (1 ·
𝐴)) = 𝐴) |
| 78 | 71, 77 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 = 𝑦) → ((0 · 𝑥) + (1 · 𝐴)) = 𝐴) |
| 79 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
| 80 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 81 | 69, 78, 79, 80 | fvmptd 7023 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((ℂ D (𝑥 ∈
ℂ ↦ (𝐴 ·
𝑥)))‘𝑦) = 𝐴) |
| 82 | 68, 81 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)) = (-(sin‘(𝐴 · 𝑦)) · 𝐴)) |
| 83 | | mulcl 11239 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
| 84 | 83 | sincld 16166 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(sin‘(𝐴 ·
𝑦)) ∈
ℂ) |
| 85 | 84 | negcld 11607 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
-(sin‘(𝐴 ·
𝑦)) ∈
ℂ) |
| 86 | 85, 80 | mulcomd 11282 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(-(sin‘(𝐴 ·
𝑦)) · 𝐴) = (𝐴 · -(sin‘(𝐴 · 𝑦)))) |
| 87 | 82, 86 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (((𝑥 ∈ ℂ ↦
-(sin‘(𝐴 ·
𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)) = (𝐴 · -(sin‘(𝐴 · 𝑦)))) |
| 88 | 58, 87 | syldan 591 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))))) → (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦)) = (𝐴 · -(sin‘(𝐴 · 𝑦)))) |
| 89 | 55, 88 | mpteq12dva 5231 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑦 ∈ (dom (𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥))) ∩ dom (ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))) ↦ (((𝑥 ∈ ℂ ↦ -(sin‘(𝐴 · 𝑥)))‘𝑦) · ((ℂ D (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
| 90 | 41, 47, 89 | 3eqtrd 2781 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((ℂ D cos) ∘ (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))) ∘f · (ℂ D
(𝑥 ∈ ℂ ↦
(𝐴 · 𝑥)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
| 91 | 9, 35, 90 | 3eqtrd 2781 |
. 2
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
| 92 | | oveq2 7439 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐴 · 𝑦) = (𝐴 · 𝑥)) |
| 93 | 92 | fveq2d 6910 |
. . . . 5
⊢ (𝑦 = 𝑥 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑥))) |
| 94 | 93 | negeqd 11502 |
. . . 4
⊢ (𝑦 = 𝑥 → -(sin‘(𝐴 · 𝑦)) = -(sin‘(𝐴 · 𝑥))) |
| 95 | 94 | oveq2d 7447 |
. . 3
⊢ (𝑦 = 𝑥 → (𝐴 · -(sin‘(𝐴 · 𝑦))) = (𝐴 · -(sin‘(𝐴 · 𝑥)))) |
| 96 | 95 | cbvmptv 5255 |
. 2
⊢ (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦)))) = (𝑥 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑥)))) |
| 97 | 91, 96 | eqtrdi 2793 |
1
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑥 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑥)))) = (𝑥 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑥))))) |