Metamath Proof Explorer

Theorem dvxpaek

Description: Derivative of the polynomial ( x + A ) ^ K . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvxpaek.s 
|- ( ph -> S e. { RR , CC } )
dvxpaek.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
dvxpaek.a 
|- ( ph -> A e. CC )
dvxpaek.k 
|- ( ph -> K e. NN )
Assertion dvxpaek 
|- ( ph -> ( S _D ( x e. X |-> ( ( x + A ) ^ K ) ) ) = ( x e. X |-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvxpaek.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvxpaek.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 dvxpaek.a 
 |-  ( ph -> A e. CC )
4 dvxpaek.k 
 |-  ( ph -> K e. NN )
5 cnelprrecn 
 |-  CC e. { RR , CC }
6 5 a1i 
 |-  ( ph -> CC e. { RR , CC } )
7 1 2 dvdmsscn 
 |-  ( ph -> X C_ CC )
8 7 adantr 
 |-  ( ( ph /\ x e. X ) -> X C_ CC )
9 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
10 8 9 sseldd 
 |-  ( ( ph /\ x e. X ) -> x e. CC )
11 3 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
12 10 11 addcld 
 |-  ( ( ph /\ x e. X ) -> ( x + A ) e. CC )
13 1red 
 |-  ( ( ph /\ x e. X ) -> 1 e. RR )
14 0red 
 |-  ( ( ph /\ x e. X ) -> 0 e. RR )
15 13 14 readdcld 
 |-  ( ( ph /\ x e. X ) -> ( 1 + 0 ) e. RR )
16 simpr 
 |-  ( ( ph /\ y e. CC ) -> y e. CC )
17 4 nnnn0d 
 |-  ( ph -> K e. NN0 )
18 17 adantr 
 |-  ( ( ph /\ y e. CC ) -> K e. NN0 )
19 16 18 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ K ) e. CC )
20 18 nn0cnd 
 |-  ( ( ph /\ y e. CC ) -> K e. CC )
21 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
22 4 21 syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
23 22 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( K - 1 ) e. NN0 )
24 16 23 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ ( K - 1 ) ) e. CC )
25 20 24 mulcld 
 |-  ( ( ph /\ y e. CC ) -> ( K x. ( y ^ ( K - 1 ) ) ) e. CC )
26 1 2 dvmptidg 
 |-  ( ph -> ( S _D ( x e. X |-> x ) ) = ( x e. X |-> 1 ) )
27 1 2 3 dvmptconst 
 |-  ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> 0 ) )
28 1 10 13 26 11 14 27 dvmptadd 
 |-  ( ph -> ( S _D ( x e. X |-> ( x + A ) ) ) = ( x e. X |-> ( 1 + 0 ) ) )
29 dvexp 
 |-  ( K e. NN -> ( CC _D ( y e. CC |-> ( y ^ K ) ) ) = ( y e. CC |-> ( K x. ( y ^ ( K - 1 ) ) ) ) )
30 4 29 syl 
 |-  ( ph -> ( CC _D ( y e. CC |-> ( y ^ K ) ) ) = ( y e. CC |-> ( K x. ( y ^ ( K - 1 ) ) ) ) )
31 oveq1 
 |-  ( y = ( x + A ) -> ( y ^ K ) = ( ( x + A ) ^ K ) )
32 oveq1 
 |-  ( y = ( x + A ) -> ( y ^ ( K - 1 ) ) = ( ( x + A ) ^ ( K - 1 ) ) )
33 32 oveq2d 
 |-  ( y = ( x + A ) -> ( K x. ( y ^ ( K - 1 ) ) ) = ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) )
34 1 6 12 15 19 25 28 30 31 33 dvmptco 
 |-  ( ph -> ( S _D ( x e. X |-> ( ( x + A ) ^ K ) ) ) = ( x e. X |-> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) ) )
35 1p0e1 
 |-  ( 1 + 0 ) = 1
36 35 oveq2i 
 |-  ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) = ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. 1 )
37 36 a1i 
 |-  ( ( ph /\ x e. X ) -> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) = ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. 1 ) )
38 4 nncnd 
 |-  ( ph -> K e. CC )
39 38 adantr 
 |-  ( ( ph /\ x e. X ) -> K e. CC )
40 22 adantr 
 |-  ( ( ph /\ x e. X ) -> ( K - 1 ) e. NN0 )
41 12 40 expcld 
 |-  ( ( ph /\ x e. X ) -> ( ( x + A ) ^ ( K - 1 ) ) e. CC )
42 39 41 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) e. CC )
43 42 mulridd 
 |-  ( ( ph /\ x e. X ) -> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. 1 ) = ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) )
44 37 43 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) = ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) )
45 44 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) ) = ( x e. X |-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )
46 34 45 eqtrd 
 |-  ( ph -> ( S _D ( x e. X |-> ( ( x + A ) ^ K ) ) ) = ( x e. X |-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )