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 ) ) ) ) ) |