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 
|- ( ( A e. CC /\ B e. CC ) -> ( CC _D ( y e. CC |-> ( A x. ( sin ` ( B x. y ) ) ) ) ) = ( y e. CC |-> ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnelprrecn 
 |-  CC e. { RR , CC }
2 1 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> CC e. { RR , CC } )
3 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> A e. CC )
4 0cnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> 0 e. CC )
5 1 a1i 
 |-  ( A e. CC -> CC e. { RR , CC } )
6 id 
 |-  ( A e. CC -> A e. CC )
7 5 6 dvmptc 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> A ) ) = ( y e. CC |-> 0 ) )
8 7 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( CC _D ( y e. CC |-> A ) ) = ( y e. CC |-> 0 ) )
9 mulcl 
 |-  ( ( B e. CC /\ y e. CC ) -> ( B x. y ) e. CC )
10 9 sincld 
 |-  ( ( B e. CC /\ y e. CC ) -> ( sin ` ( B x. y ) ) e. CC )
11 10 adantll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( sin ` ( B x. y ) ) e. CC )
12 simpl 
 |-  ( ( B e. CC /\ y e. CC ) -> B e. CC )
13 9 coscld 
 |-  ( ( B e. CC /\ y e. CC ) -> ( cos ` ( B x. y ) ) e. CC )
14 12 13 mulcld 
 |-  ( ( B e. CC /\ y e. CC ) -> ( B x. ( cos ` ( B x. y ) ) ) e. CC )
15 14 adantll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( B x. ( cos ` ( B x. y ) ) ) e. CC )
16 dvsinax 
 |-  ( B e. CC -> ( CC _D ( y e. CC |-> ( sin ` ( B x. y ) ) ) ) = ( y e. CC |-> ( B x. ( cos ` ( B x. y ) ) ) ) )
17 16 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( CC _D ( y e. CC |-> ( sin ` ( B x. y ) ) ) ) = ( y e. CC |-> ( B x. ( cos ` ( B x. y ) ) ) ) )
18 2 3 4 8 11 15 17 dvmptmul 
 |-  ( ( A e. CC /\ B e. CC ) -> ( CC _D ( y e. CC |-> ( A x. ( sin ` ( B x. y ) ) ) ) ) = ( y e. CC |-> ( ( 0 x. ( sin ` ( B x. y ) ) ) + ( ( B x. ( cos ` ( B x. y ) ) ) x. A ) ) ) )
19 11 mul02d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( 0 x. ( sin ` ( B x. y ) ) ) = 0 )
20 12 adantll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> B e. CC )
21 13 adantll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( cos ` ( B x. y ) ) e. CC )
22 20 21 3 mul32d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( ( B x. ( cos ` ( B x. y ) ) ) x. A ) = ( ( B x. A ) x. ( cos ` ( B x. y ) ) ) )
23 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
24 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
25 23 24 mulcomd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B x. A ) = ( A x. B ) )
26 25 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( B x. A ) = ( A x. B ) )
27 26 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( ( B x. A ) x. ( cos ` ( B x. y ) ) ) = ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) )
28 22 27 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( ( B x. ( cos ` ( B x. y ) ) ) x. A ) = ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) )
29 19 28 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( ( 0 x. ( sin ` ( B x. y ) ) ) + ( ( B x. ( cos ` ( B x. y ) ) ) x. A ) ) = ( 0 + ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) ) )
30 3 20 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( A x. B ) e. CC )
31 30 21 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) e. CC )
32 31 addid2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( 0 + ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) ) = ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) )
33 29 32 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ y e. CC ) -> ( ( 0 x. ( sin ` ( B x. y ) ) ) + ( ( B x. ( cos ` ( B x. y ) ) ) x. A ) ) = ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) )
34 33 mpteq2dva 
 |-  ( ( A e. CC /\ B e. CC ) -> ( y e. CC |-> ( ( 0 x. ( sin ` ( B x. y ) ) ) + ( ( B x. ( cos ` ( B x. y ) ) ) x. A ) ) ) = ( y e. CC |-> ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) ) )
35 18 34 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( CC _D ( y e. CC |-> ( A x. ( sin ` ( B x. y ) ) ) ) ) = ( y e. CC |-> ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) ) )