Metamath Proof Explorer

Theorem dvsinexp

Description: The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis dvsinexp.5 
|- ( ph -> N e. NN )
Assertion dvsinexp 
|- ( ph -> ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ) = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 dvsinexp.5 
 |-  ( ph -> N e. NN )
2 cnelprrecn 
 |-  CC e. { RR , CC }
3 2 a1i 
 |-  ( ph -> CC e. { RR , CC } )
4 sinf 
 |-  sin : CC --> CC
5 4 a1i 
 |-  ( ph -> sin : CC --> CC )
6 5 ffvelrnda 
 |-  ( ( ph /\ x e. CC ) -> ( sin ` x ) e. CC )
7 cosf 
 |-  cos : CC --> CC
8 7 a1i 
 |-  ( ph -> cos : CC --> CC )
9 8 ffvelrnda 
 |-  ( ( ph /\ x e. CC ) -> ( cos ` x ) e. CC )
10 simpr 
 |-  ( ( ph /\ y e. CC ) -> y e. CC )
11 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
12 11 adantr 
 |-  ( ( ph /\ y e. CC ) -> N e. NN0 )
13 10 12 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ N ) e. CC )
14 1 nncnd 
 |-  ( ph -> N e. CC )
15 14 adantr 
 |-  ( ( ph /\ y e. CC ) -> N e. CC )
16 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
17 1 16 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
18 17 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( N - 1 ) e. NN0 )
19 10 18 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ ( N - 1 ) ) e. CC )
20 15 19 mulcld 
 |-  ( ( ph /\ y e. CC ) -> ( N x. ( y ^ ( N - 1 ) ) ) e. CC )
21 dvsin 
 |-  ( CC _D sin ) = cos
22 5 feqmptd 
 |-  ( ph -> sin = ( x e. CC |-> ( sin ` x ) ) )
23 22 oveq2d 
 |-  ( ph -> ( CC _D sin ) = ( CC _D ( x e. CC |-> ( sin ` x ) ) ) )
24 8 feqmptd 
 |-  ( ph -> cos = ( x e. CC |-> ( cos ` x ) ) )
25 21 23 24 3eqtr3a 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) ) )
26 dvexp 
 |-  ( N e. NN -> ( CC _D ( y e. CC |-> ( y ^ N ) ) ) = ( y e. CC |-> ( N x. ( y ^ ( N - 1 ) ) ) ) )
27 1 26 syl 
 |-  ( ph -> ( CC _D ( y e. CC |-> ( y ^ N ) ) ) = ( y e. CC |-> ( N x. ( y ^ ( N - 1 ) ) ) ) )
28 oveq1 
 |-  ( y = ( sin ` x ) -> ( y ^ N ) = ( ( sin ` x ) ^ N ) )
29 oveq1 
 |-  ( y = ( sin ` x ) -> ( y ^ ( N - 1 ) ) = ( ( sin ` x ) ^ ( N - 1 ) ) )
30 29 oveq2d 
 |-  ( y = ( sin ` x ) -> ( N x. ( y ^ ( N - 1 ) ) ) = ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
31 3 3 6 9 13 20 25 27 28 30 dvmptco 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ) = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )