Metamath Proof Explorer


Theorem dvasinbx

Description: Derivative exercise: the derivative with respect to y of A x sin(By), given two constants A and B . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dvasinbx ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnelprrecn ℂ ∈ { ℝ , ℂ }
2 1 a1i ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ℂ ∈ { ℝ , ℂ } )
3 simpll ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
4 0cnd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → 0 ∈ ℂ )
5 1 a1i ( 𝐴 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
6 id ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
7 5 6 dvmptc ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑦 ∈ ℂ ↦ 0 ) )
8 7 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑦 ∈ ℂ ↦ 0 ) )
9 mulcl ( ( 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐵 · 𝑦 ) ∈ ℂ )
10 9 sincld ( ( 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( 𝐵 · 𝑦 ) ) ∈ ℂ )
11 10 adantll ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( sin ‘ ( 𝐵 · 𝑦 ) ) ∈ ℂ )
12 simpl ( ( 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝐵 ∈ ℂ )
13 9 coscld ( ( 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( 𝐵 · 𝑦 ) ) ∈ ℂ )
14 12 13 mulcld ( ( 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ∈ ℂ )
15 14 adantll ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ∈ ℂ )
16 dvsinax ( 𝐵 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐵 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) )
17 16 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐵 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) )
18 2 3 4 8 11 15 17 dvmptmul ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 0 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) + ( ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) · 𝐴 ) ) ) )
19 11 mul02d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 0 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) = 0 )
20 12 adantll ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → 𝐵 ∈ ℂ )
21 13 adantll ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( cos ‘ ( 𝐵 · 𝑦 ) ) ∈ ℂ )
22 20 21 3 mul32d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) · 𝐴 ) = ( ( 𝐵 · 𝐴 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) )
23 simpr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
24 simpl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
25 23 24 mulcomd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
26 25 adantr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
27 26 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐵 · 𝐴 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) = ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) )
28 22 27 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) · 𝐴 ) = ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) )
29 19 28 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 0 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) + ( ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) · 𝐴 ) ) = ( 0 + ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) )
30 3 20 mulcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
31 30 21 mulcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ∈ ℂ )
32 31 addid2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 0 + ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) = ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) )
33 29 32 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( ( 0 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) + ( ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) · 𝐴 ) ) = ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) )
34 33 mpteq2dva ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑦 ∈ ℂ ↦ ( ( 0 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) + ( ( 𝐵 · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) · 𝐴 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) )
35 18 34 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( sin ‘ ( 𝐵 · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 · 𝐵 ) · ( cos ‘ ( 𝐵 · 𝑦 ) ) ) ) )