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