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