Metamath Proof Explorer

Theorem dvexp3

Description: Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion dvexp3 
|- ( N e. ZZ -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
2 cnelprrecn 
 |-  CC e. { RR , CC }
3 2 a1i 
 |-  ( N e. NN0 -> CC e. { RR , CC } )
4 expcl 
 |-  ( ( x e. CC /\ N e. NN0 ) -> ( x ^ N ) e. CC )
5 4 ancoms 
 |-  ( ( N e. NN0 /\ x e. CC ) -> ( x ^ N ) e. CC )
6 c0ex 
 |-  0 e. _V
7 ovex 
 |-  ( N x. ( x ^ ( N - 1 ) ) ) e. _V
8 6 7 ifex 
 |-  if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) e. _V
9 8 a1i 
 |-  ( ( N e. NN0 /\ x e. CC ) -> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) e. _V )
10 dvexp2 
 |-  ( N e. NN0 -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
11 difssd 
 |-  ( N e. NN0 -> ( CC \ { 0 } ) C_ CC )
12 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
13 12 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
14 13 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
15 cnn0opn 
 |-  ( CC \ { 0 } ) e. ( TopOpen ` CCfld )
16 15 a1i 
 |-  ( N e. NN0 -> ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) )
17 3 5 9 10 11 14 12 16 dvmptres 
 |-  ( N e. NN0 -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
18 ifid 
 |-  if ( N = 0 , ( N x. ( x ^ ( N - 1 ) ) ) , ( N x. ( x ^ ( N - 1 ) ) ) ) = ( N x. ( x ^ ( N - 1 ) ) )
19 id 
 |-  ( N = 0 -> N = 0 )
20 oveq1 
 |-  ( N = 0 -> ( N - 1 ) = ( 0 - 1 ) )
21 20 oveq2d 
 |-  ( N = 0 -> ( x ^ ( N - 1 ) ) = ( x ^ ( 0 - 1 ) ) )
22 19 21 oveq12d 
 |-  ( N = 0 -> ( N x. ( x ^ ( N - 1 ) ) ) = ( 0 x. ( x ^ ( 0 - 1 ) ) ) )
23 eldifsn 
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
24 0z 
 |-  0 e. ZZ
25 peano2zm 
 |-  ( 0 e. ZZ -> ( 0 - 1 ) e. ZZ )
26 24 25 ax-mp 
 |-  ( 0 - 1 ) e. ZZ
27 expclz 
 |-  ( ( x e. CC /\ x =/= 0 /\ ( 0 - 1 ) e. ZZ ) -> ( x ^ ( 0 - 1 ) ) e. CC )
28 26 27 mp3an3 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( x ^ ( 0 - 1 ) ) e. CC )
29 23 28 sylbi 
 |-  ( x e. ( CC \ { 0 } ) -> ( x ^ ( 0 - 1 ) ) e. CC )
30 29 adantl 
 |-  ( ( N e. NN0 /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( 0 - 1 ) ) e. CC )
31 30 mul02d 
 |-  ( ( N e. NN0 /\ x e. ( CC \ { 0 } ) ) -> ( 0 x. ( x ^ ( 0 - 1 ) ) ) = 0 )
32 22 31 sylan9eqr 
 |-  ( ( ( N e. NN0 /\ x e. ( CC \ { 0 } ) ) /\ N = 0 ) -> ( N x. ( x ^ ( N - 1 ) ) ) = 0 )
33 32 ifeq1da 
 |-  ( ( N e. NN0 /\ x e. ( CC \ { 0 } ) ) -> if ( N = 0 , ( N x. ( x ^ ( N - 1 ) ) ) , ( N x. ( x ^ ( N - 1 ) ) ) ) = if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) )
34 18 33 eqtr3id 
 |-  ( ( N e. NN0 /\ x e. ( CC \ { 0 } ) ) -> ( N x. ( x ^ ( N - 1 ) ) ) = if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) )
35 34 mpteq2dva 
 |-  ( N e. NN0 -> ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) = ( x e. ( CC \ { 0 } ) |-> if ( N = 0 , 0 , ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
36 17 35 eqtr4d 
 |-  ( N e. NN0 -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
37 eldifi 
 |-  ( x e. ( CC \ { 0 } ) -> x e. CC )
38 37 adantl 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> x e. CC )
39 simpll 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> N e. RR )
40 39 recnd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> N e. CC )
41 nnnn0 
 |-  ( -u N e. NN -> -u N e. NN0 )
42 41 ad2antlr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> -u N e. NN0 )
43 expneg2 
 |-  ( ( x e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( x ^ N ) = ( 1 / ( x ^ -u N ) ) )
44 38 40 42 43 syl3anc 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ N ) = ( 1 / ( x ^ -u N ) ) )
45 44 mpteq2dva 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) = ( x e. ( CC \ { 0 } ) |-> ( 1 / ( x ^ -u N ) ) ) )
46 45 oveq2d 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( CC _D ( x e. ( CC \ { 0 } ) |-> ( 1 / ( x ^ -u N ) ) ) ) )
47 2 a1i 
 |-  ( ( N e. RR /\ -u N e. NN ) -> CC e. { RR , CC } )
48 eldifsni 
 |-  ( x e. ( CC \ { 0 } ) -> x =/= 0 )
49 48 adantl 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> x =/= 0 )
50 nnz 
 |-  ( -u N e. NN -> -u N e. ZZ )
51 50 ad2antlr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> -u N e. ZZ )
52 38 49 51 expclzd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ -u N ) e. CC )
53 38 49 51 expne0d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ -u N ) =/= 0 )
54 eldifsn 
 |-  ( ( x ^ -u N ) e. ( CC \ { 0 } ) <-> ( ( x ^ -u N ) e. CC /\ ( x ^ -u N ) =/= 0 ) )
55 52 53 54 sylanbrc 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ -u N ) e. ( CC \ { 0 } ) )
56 ovex 
 |-  ( -u N x. ( x ^ ( -u N - 1 ) ) ) e. _V
57 56 a1i 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N x. ( x ^ ( -u N - 1 ) ) ) e. _V )
58 simpr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ y e. ( CC \ { 0 } ) ) -> y e. ( CC \ { 0 } ) )
59 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
60 58 59 sylib 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ y e. ( CC \ { 0 } ) ) -> ( y e. CC /\ y =/= 0 ) )
61 reccl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( 1 / y ) e. CC )
62 60 61 syl 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ y e. ( CC \ { 0 } ) ) -> ( 1 / y ) e. CC )
63 negex 
 |-  -u ( 1 / ( y ^ 2 ) ) e. _V
64 63 a1i 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ y e. ( CC \ { 0 } ) ) -> -u ( 1 / ( y ^ 2 ) ) e. _V )
65 simpr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. CC ) -> x e. CC )
66 41 ad2antlr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. CC ) -> -u N e. NN0 )
67 65 66 expcld 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. CC ) -> ( x ^ -u N ) e. CC )
68 56 a1i 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. CC ) -> ( -u N x. ( x ^ ( -u N - 1 ) ) ) e. _V )
69 dvexp 
 |-  ( -u N e. NN -> ( CC _D ( x e. CC |-> ( x ^ -u N ) ) ) = ( x e. CC |-> ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) )
70 69 adantl 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC _D ( x e. CC |-> ( x ^ -u N ) ) ) = ( x e. CC |-> ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) )
71 difssd 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC \ { 0 } ) C_ CC )
72 15 a1i 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) )
73 47 67 68 70 71 14 12 72 dvmptres 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ -u N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) )
74 ax-1cn 
 |-  1 e. CC
75 dvrec 
 |-  ( 1 e. CC -> ( CC _D ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ) = ( y e. ( CC \ { 0 } ) |-> -u ( 1 / ( y ^ 2 ) ) ) )
76 74 75 mp1i 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC _D ( y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) ) = ( y e. ( CC \ { 0 } ) |-> -u ( 1 / ( y ^ 2 ) ) ) )
77 oveq2 
 |-  ( y = ( x ^ -u N ) -> ( 1 / y ) = ( 1 / ( x ^ -u N ) ) )
78 oveq1 
 |-  ( y = ( x ^ -u N ) -> ( y ^ 2 ) = ( ( x ^ -u N ) ^ 2 ) )
79 78 oveq2d 
 |-  ( y = ( x ^ -u N ) -> ( 1 / ( y ^ 2 ) ) = ( 1 / ( ( x ^ -u N ) ^ 2 ) ) )
80 79 negeqd 
 |-  ( y = ( x ^ -u N ) -> -u ( 1 / ( y ^ 2 ) ) = -u ( 1 / ( ( x ^ -u N ) ^ 2 ) ) )
81 47 47 55 57 62 64 73 76 77 80 dvmptco 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( 1 / ( x ^ -u N ) ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( -u ( 1 / ( ( x ^ -u N ) ^ 2 ) ) x. ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) ) )
82 2z 
 |-  2 e. ZZ
83 82 a1i 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> 2 e. ZZ )
84 expmulz 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( -u N e. ZZ /\ 2 e. ZZ ) ) -> ( x ^ ( -u N x. 2 ) ) = ( ( x ^ -u N ) ^ 2 ) )
85 38 49 51 83 84 syl22anc 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( -u N x. 2 ) ) = ( ( x ^ -u N ) ^ 2 ) )
86 85 eqcomd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( x ^ -u N ) ^ 2 ) = ( x ^ ( -u N x. 2 ) ) )
87 86 oveq2d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( 1 / ( ( x ^ -u N ) ^ 2 ) ) = ( 1 / ( x ^ ( -u N x. 2 ) ) ) )
88 87 negeqd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> -u ( 1 / ( ( x ^ -u N ) ^ 2 ) ) = -u ( 1 / ( x ^ ( -u N x. 2 ) ) ) )
89 peano2zm 
 |-  ( -u N e. ZZ -> ( -u N - 1 ) e. ZZ )
90 51 89 syl 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N - 1 ) e. ZZ )
91 38 49 90 expclzd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( -u N - 1 ) ) e. CC )
92 40 91 mulneg1d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N x. ( x ^ ( -u N - 1 ) ) ) = -u ( N x. ( x ^ ( -u N - 1 ) ) ) )
93 88 92 oveq12d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u ( 1 / ( ( x ^ -u N ) ^ 2 ) ) x. ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) = ( -u ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. -u ( N x. ( x ^ ( -u N - 1 ) ) ) ) )
94 zmulcl 
 |-  ( ( -u N e. ZZ /\ 2 e. ZZ ) -> ( -u N x. 2 ) e. ZZ )
95 51 82 94 sylancl 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N x. 2 ) e. ZZ )
96 38 49 95 expclzd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( -u N x. 2 ) ) e. CC )
97 38 49 95 expne0d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( -u N x. 2 ) ) =/= 0 )
98 96 97 reccld 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( 1 / ( x ^ ( -u N x. 2 ) ) ) e. CC )
99 40 91 mulcld 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( N x. ( x ^ ( -u N - 1 ) ) ) e. CC )
100 98 99 mul2negd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. -u ( N x. ( x ^ ( -u N - 1 ) ) ) ) = ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( N x. ( x ^ ( -u N - 1 ) ) ) ) )
101 98 40 91 mul12d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( N x. ( x ^ ( -u N - 1 ) ) ) ) = ( N x. ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( x ^ ( -u N - 1 ) ) ) ) )
102 38 49 95 90 expsubd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( ( -u N - 1 ) - ( -u N x. 2 ) ) ) = ( ( x ^ ( -u N - 1 ) ) / ( x ^ ( -u N x. 2 ) ) ) )
103 nncn 
 |-  ( -u N e. NN -> -u N e. CC )
104 103 ad2antlr 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> -u N e. CC )
105 74 a1i 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> 1 e. CC )
106 95 zcnd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N x. 2 ) e. CC )
107 104 105 106 sub32d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( -u N - 1 ) - ( -u N x. 2 ) ) = ( ( -u N - ( -u N x. 2 ) ) - 1 ) )
108 104 times2d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N x. 2 ) = ( -u N + -u N ) )
109 104 40 negsubd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N + -u N ) = ( -u N - N ) )
110 108 109 eqtrd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N x. 2 ) = ( -u N - N ) )
111 110 oveq2d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N - ( -u N x. 2 ) ) = ( -u N - ( -u N - N ) ) )
112 104 40 nncand 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N - ( -u N - N ) ) = N )
113 111 112 eqtrd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u N - ( -u N x. 2 ) ) = N )
114 113 oveq1d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( -u N - ( -u N x. 2 ) ) - 1 ) = ( N - 1 ) )
115 107 114 eqtrd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( -u N - 1 ) - ( -u N x. 2 ) ) = ( N - 1 ) )
116 115 oveq2d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( x ^ ( ( -u N - 1 ) - ( -u N x. 2 ) ) ) = ( x ^ ( N - 1 ) ) )
117 91 96 97 divrec2d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( x ^ ( -u N - 1 ) ) / ( x ^ ( -u N x. 2 ) ) ) = ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( x ^ ( -u N - 1 ) ) ) )
118 102 116 117 3eqtr3rd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( x ^ ( -u N - 1 ) ) ) = ( x ^ ( N - 1 ) ) )
119 118 oveq2d 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( N x. ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( x ^ ( -u N - 1 ) ) ) ) = ( N x. ( x ^ ( N - 1 ) ) ) )
120 101 119 eqtrd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( ( 1 / ( x ^ ( -u N x. 2 ) ) ) x. ( N x. ( x ^ ( -u N - 1 ) ) ) ) = ( N x. ( x ^ ( N - 1 ) ) ) )
121 93 100 120 3eqtrd 
 |-  ( ( ( N e. RR /\ -u N e. NN ) /\ x e. ( CC \ { 0 } ) ) -> ( -u ( 1 / ( ( x ^ -u N ) ^ 2 ) ) x. ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) = ( N x. ( x ^ ( N - 1 ) ) ) )
122 121 mpteq2dva 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( x e. ( CC \ { 0 } ) |-> ( -u ( 1 / ( ( x ^ -u N ) ^ 2 ) ) x. ( -u N x. ( x ^ ( -u N - 1 ) ) ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
123 46 81 122 3eqtrd 
 |-  ( ( N e. RR /\ -u N e. NN ) -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
124 36 123 jaoi 
 |-  ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
125 1 124 sylbi 
 |-  ( N e. ZZ -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( x ^ N ) ) ) = ( x e. ( CC \ { 0 } ) |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )