Metamath Proof Explorer

Theorem dvcosax

Description: Derivative exercise: the derivative with respect to x of cos(Ax), given a constant A . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dvcosax ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
2 eqidd ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) )
3 cosf ⊢ cos : ℂ ⟶ ℂ
4 3 a1i ⊢ ( 𝐴 ∈ ℂ → cos : ℂ ⟶ ℂ )
5 4 feqmptd ⊢ ( 𝐴 ∈ ℂ → cos = ( 𝑦 ∈ ℂ ↦ ( cos ‘ 𝑦 ) ) )
6 fveq2 ⊢ ( 𝑦 = ( 𝐴 · 𝑥 ) → ( cos ‘ 𝑦 ) = ( cos ‘ ( 𝐴 · 𝑥 ) ) )
7 1 2 5 6 fmptco ⊢ ( 𝐴 ∈ ℂ → ( cos ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑥 ) ) ) )
8 7 eqcomd ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑥 ) ) ) = ( cos ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) )
9 8 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑥 ) ) ) ) = ( ℂ D ( cos ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) )
10 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
11 10 a1i ⊢ ( 𝐴 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
12 1 fmpttd ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) : ℂ ⟶ ℂ )
13 dvcos ⊢ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )
14 13 dmeqi ⊢ dom ( ℂ D cos ) = dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )
15 dmmptg ⊢ ( ∀ 𝑥 ∈ ℂ - ( sin ‘ 𝑥 ) ∈ ℂ → dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) = ℂ )
16 sincl ⊢ ( 𝑥 ∈ ℂ → ( sin ‘ 𝑥 ) ∈ ℂ )
17 16 negcld ⊢ ( 𝑥 ∈ ℂ → - ( sin ‘ 𝑥 ) ∈ ℂ )
18 15 17 mprg ⊢ dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) = ℂ
19 14 18 eqtri ⊢ dom ( ℂ D cos ) = ℂ
20 19 a1i ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D cos ) = ℂ )
21 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ ℂ )
22 0red ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℝ )
23 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
24 11 23 dvmptc ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
25 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
26 1red ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℝ )
27 11 dvmptid ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
28 11 21 22 24 25 26 27 dvmptmul ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ) )
29 28 dmeqd ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) = dom ( 𝑥 ∈ ℂ ↦ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ) )
30 dmmptg ⊢ ( ∀ 𝑥 ∈ ℂ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ∈ V → dom ( 𝑥 ∈ ℂ ↦ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ) = ℂ )
31 ovex ⊢ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ∈ V
32 31 a1i ⊢ ( 𝑥 ∈ ℂ → ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ∈ V )
33 30 32 mprg ⊢ dom ( 𝑥 ∈ ℂ ↦ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ) = ℂ
34 29 33 eqtrdi ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) = ℂ )
35 11 11 4 12 20 34 dvcof ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( cos ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( ( ( ℂ D cos ) ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) )
36 dvcos ⊢ ( ℂ D cos ) = ( 𝑦 ∈ ℂ ↦ - ( sin ‘ 𝑦 ) )
37 36 a1i ⊢ ( 𝐴 ∈ ℂ → ( ℂ D cos ) = ( 𝑦 ∈ ℂ ↦ - ( sin ‘ 𝑦 ) ) )
38 fveq2 ⊢ ( 𝑦 = ( 𝐴 · 𝑥 ) → ( sin ‘ 𝑦 ) = ( sin ‘ ( 𝐴 · 𝑥 ) ) )
39 38 negeqd ⊢ ( 𝑦 = ( 𝐴 · 𝑥 ) → - ( sin ‘ 𝑦 ) = - ( sin ‘ ( 𝐴 · 𝑥 ) ) )
40 1 2 37 39 fmptco ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ D cos ) ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) )
41 40 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℂ D cos ) ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) )
42 cnex ⊢ ℂ ∈ V
43 42 mptex ⊢ ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∈ V
44 ovex ⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ∈ V
45 offval3 ⊢ ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∈ V ∧ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ∈ V ) → ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ↦ ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) ) )
46 43 44 45 mp2an ⊢ ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ↦ ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) )
47 46 a1i ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ↦ ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) ) )
48 1 sincld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( sin ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
49 48 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → - ( sin ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
50 49 ralrimiva ⊢ ( 𝐴 ∈ ℂ → ∀ 𝑥 ∈ ℂ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ )
51 dmmptg ⊢ ( ∀ 𝑥 ∈ ℂ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ∈ ℂ → dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) = ℂ )
52 50 51 syl ⊢ ( 𝐴 ∈ ℂ → dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) = ℂ )
53 52 34 ineq12d ⊢ ( 𝐴 ∈ ℂ → ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( ℂ ∩ ℂ ) )
54 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
55 53 54 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ℂ )
56 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ) → 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) )
57 55 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ) → ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ℂ )
58 56 57 eleqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ) → 𝑦 ∈ ℂ )
59 eqidd ⊢ ( 𝑦 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) )
60 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑦 ) )
61 60 fveq2d ⊢ ( 𝑥 = 𝑦 → ( sin ‘ ( 𝐴 · 𝑥 ) ) = ( sin ‘ ( 𝐴 · 𝑦 ) ) )
62 61 negeqd ⊢ ( 𝑥 = 𝑦 → - ( sin ‘ ( 𝐴 · 𝑥 ) ) = - ( sin ‘ ( 𝐴 · 𝑦 ) ) )
63 62 adantl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 = 𝑦 ) → - ( sin ‘ ( 𝐴 · 𝑥 ) ) = - ( sin ‘ ( 𝐴 · 𝑦 ) ) )
64 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
65 negex ⊢ - ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ V
66 65 a1i ⊢ ( 𝑦 ∈ ℂ → - ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ V )
67 59 63 64 66 fvmptd ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) = - ( sin ‘ ( 𝐴 · 𝑦 ) ) )
68 67 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) = - ( sin ‘ ( 𝐴 · 𝑦 ) ) )
69 28 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) ) )
70 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 0 · 𝑥 ) = ( 0 · 𝑦 ) )
71 70 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) = ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) )
72 mul02 ⊢ ( 𝑦 ∈ ℂ → ( 0 · 𝑦 ) = 0 )
73 mullid ⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
74 72 73 oveqan12rd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) = ( 0 + 𝐴 ) )
75 addlid ⊢ ( 𝐴 ∈ ℂ → ( 0 + 𝐴 ) = 𝐴 )
76 75 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 + 𝐴 ) = 𝐴 )
77 74 76 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) = 𝐴 )
78 71 77 sylan9eqr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑥 = 𝑦 ) → ( ( 0 · 𝑥 ) + ( 1 · 𝐴 ) ) = 𝐴 )
79 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
80 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
81 69 78 79 80 fvmptd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) = 𝐴 )
82 68 81 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( - ( sin ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) )
83 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
84 83 sincld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
85 84 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → - ( sin ‘ ( 𝐴 · 𝑦 ) ) ∈ ℂ )
86 85 80 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( - ( sin ‘ ( 𝐴 · 𝑦 ) ) · 𝐴 ) = ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
87 82 86 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
88 58 87 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ) → ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
89 55 88 mpteq12dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ( dom ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ∩ dom ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) ↦ ( ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) · ( ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
90 41 47 89 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℂ D cos ) ∘ ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ∘f · ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
91 9 35 90 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) )
92 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑥 ) )
93 92 fveq2d ⊢ ( 𝑦 = 𝑥 → ( sin ‘ ( 𝐴 · 𝑦 ) ) = ( sin ‘ ( 𝐴 · 𝑥 ) ) )
94 93 negeqd ⊢ ( 𝑦 = 𝑥 → - ( sin ‘ ( 𝐴 · 𝑦 ) ) = - ( sin ‘ ( 𝐴 · 𝑥 ) ) )
95 94 oveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) = ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) )
96 95 cbvmptv ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) )
97 91 96 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( 𝐴 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝐴 · - ( sin ‘ ( 𝐴 · 𝑥 ) ) ) ) )