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 addlidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℂ ) → ( 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 ‘ ( 𝐵 · 𝑦 ) ) ) ) )