Metamath Proof Explorer

Theorem dvexp

Description: Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvexp 
|- ( N e. NN -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = 1 -> ( x ^ n ) = ( x ^ 1 ) )
2 1 mpteq2dv 
 |-  ( n = 1 -> ( x e. CC |-> ( x ^ n ) ) = ( x e. CC |-> ( x ^ 1 ) ) )
3 2 oveq2d 
 |-  ( n = 1 -> ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( CC _D ( x e. CC |-> ( x ^ 1 ) ) ) )
4 id 
 |-  ( n = 1 -> n = 1 )
5 oveq1 
 |-  ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
6 5 oveq2d 
 |-  ( n = 1 -> ( x ^ ( n - 1 ) ) = ( x ^ ( 1 - 1 ) ) )
7 4 6 oveq12d 
 |-  ( n = 1 -> ( n x. ( x ^ ( n - 1 ) ) ) = ( 1 x. ( x ^ ( 1 - 1 ) ) ) )
8 7 mpteq2dv 
 |-  ( n = 1 -> ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) = ( x e. CC |-> ( 1 x. ( x ^ ( 1 - 1 ) ) ) ) )
9 3 8 eqeq12d 
 |-  ( n = 1 -> ( ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) <-> ( CC _D ( x e. CC |-> ( x ^ 1 ) ) ) = ( x e. CC |-> ( 1 x. ( x ^ ( 1 - 1 ) ) ) ) ) )
10 oveq2 
 |-  ( n = k -> ( x ^ n ) = ( x ^ k ) )
11 10 mpteq2dv 
 |-  ( n = k -> ( x e. CC |-> ( x ^ n ) ) = ( x e. CC |-> ( x ^ k ) ) )
12 11 oveq2d 
 |-  ( n = k -> ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( CC _D ( x e. CC |-> ( x ^ k ) ) ) )
13 id 
 |-  ( n = k -> n = k )
14 oveq1 
 |-  ( n = k -> ( n - 1 ) = ( k - 1 ) )
15 14 oveq2d 
 |-  ( n = k -> ( x ^ ( n - 1 ) ) = ( x ^ ( k - 1 ) ) )
16 13 15 oveq12d 
 |-  ( n = k -> ( n x. ( x ^ ( n - 1 ) ) ) = ( k x. ( x ^ ( k - 1 ) ) ) )
17 16 mpteq2dv 
 |-  ( n = k -> ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) )
18 12 17 eqeq12d 
 |-  ( n = k -> ( ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) <-> ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) )
19 oveq2 
 |-  ( n = ( k + 1 ) -> ( x ^ n ) = ( x ^ ( k + 1 ) ) )
20 19 mpteq2dv 
 |-  ( n = ( k + 1 ) -> ( x e. CC |-> ( x ^ n ) ) = ( x e. CC |-> ( x ^ ( k + 1 ) ) ) )
21 20 oveq2d 
 |-  ( n = ( k + 1 ) -> ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( CC _D ( x e. CC |-> ( x ^ ( k + 1 ) ) ) ) )
22 id 
 |-  ( n = ( k + 1 ) -> n = ( k + 1 ) )
23 oveq1 
 |-  ( n = ( k + 1 ) -> ( n - 1 ) = ( ( k + 1 ) - 1 ) )
24 23 oveq2d 
 |-  ( n = ( k + 1 ) -> ( x ^ ( n - 1 ) ) = ( x ^ ( ( k + 1 ) - 1 ) ) )
25 22 24 oveq12d 
 |-  ( n = ( k + 1 ) -> ( n x. ( x ^ ( n - 1 ) ) ) = ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) )
26 25 mpteq2dv 
 |-  ( n = ( k + 1 ) -> ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) = ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) )
27 21 26 eqeq12d 
 |-  ( n = ( k + 1 ) -> ( ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) <-> ( CC _D ( x e. CC |-> ( x ^ ( k + 1 ) ) ) ) = ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) ) )
28 oveq2 
 |-  ( n = N -> ( x ^ n ) = ( x ^ N ) )
29 28 mpteq2dv 
 |-  ( n = N -> ( x e. CC |-> ( x ^ n ) ) = ( x e. CC |-> ( x ^ N ) ) )
30 29 oveq2d 
 |-  ( n = N -> ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( CC _D ( x e. CC |-> ( x ^ N ) ) ) )
31 id 
 |-  ( n = N -> n = N )
32 oveq1 
 |-  ( n = N -> ( n - 1 ) = ( N - 1 ) )
33 32 oveq2d 
 |-  ( n = N -> ( x ^ ( n - 1 ) ) = ( x ^ ( N - 1 ) ) )
34 31 33 oveq12d 
 |-  ( n = N -> ( n x. ( x ^ ( n - 1 ) ) ) = ( N x. ( x ^ ( N - 1 ) ) ) )
35 34 mpteq2dv 
 |-  ( n = N -> ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )
36 30 35 eqeq12d 
 |-  ( n = N -> ( ( CC _D ( x e. CC |-> ( x ^ n ) ) ) = ( x e. CC |-> ( n x. ( x ^ ( n - 1 ) ) ) ) <-> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) ) )
37 exp1 
 |-  ( x e. CC -> ( x ^ 1 ) = x )
38 37 mpteq2ia 
 |-  ( x e. CC |-> ( x ^ 1 ) ) = ( x e. CC |-> x )
39 mptresid 
 |-  ( _I |` CC ) = ( x e. CC |-> x )
40 38 39 eqtr4i 
 |-  ( x e. CC |-> ( x ^ 1 ) ) = ( _I |` CC )
41 40 oveq2i 
 |-  ( CC _D ( x e. CC |-> ( x ^ 1 ) ) ) = ( CC _D ( _I |` CC ) )
42 1m1e0 
 |-  ( 1 - 1 ) = 0
43 42 oveq2i 
 |-  ( x ^ ( 1 - 1 ) ) = ( x ^ 0 )
44 exp0 
 |-  ( x e. CC -> ( x ^ 0 ) = 1 )
45 43 44 eqtrid 
 |-  ( x e. CC -> ( x ^ ( 1 - 1 ) ) = 1 )
46 45 oveq2d 
 |-  ( x e. CC -> ( 1 x. ( x ^ ( 1 - 1 ) ) ) = ( 1 x. 1 ) )
47 1t1e1 
 |-  ( 1 x. 1 ) = 1
48 46 47 eqtrdi 
 |-  ( x e. CC -> ( 1 x. ( x ^ ( 1 - 1 ) ) ) = 1 )
49 48 mpteq2ia 
 |-  ( x e. CC |-> ( 1 x. ( x ^ ( 1 - 1 ) ) ) ) = ( x e. CC |-> 1 )
50 fconstmpt 
 |-  ( CC X. { 1 } ) = ( x e. CC |-> 1 )
51 49 50 eqtr4i 
 |-  ( x e. CC |-> ( 1 x. ( x ^ ( 1 - 1 ) ) ) ) = ( CC X. { 1 } )
52 dvid 
 |-  ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
53 51 52 eqtr4i 
 |-  ( x e. CC |-> ( 1 x. ( x ^ ( 1 - 1 ) ) ) ) = ( CC _D ( _I |` CC ) )
54 41 53 eqtr4i 
 |-  ( CC _D ( x e. CC |-> ( x ^ 1 ) ) ) = ( x e. CC |-> ( 1 x. ( x ^ ( 1 - 1 ) ) ) )
55 nncn 
 |-  ( k e. NN -> k e. CC )
56 55 adantr 
 |-  ( ( k e. NN /\ x e. CC ) -> k e. CC )
57 ax-1cn 
 |-  1 e. CC
58 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
59 56 57 58 sylancl 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k + 1 ) - 1 ) = k )
60 59 oveq2d 
 |-  ( ( k e. NN /\ x e. CC ) -> ( x ^ ( ( k + 1 ) - 1 ) ) = ( x ^ k ) )
61 60 oveq2d 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) = ( ( k + 1 ) x. ( x ^ k ) ) )
62 57 a1i 
 |-  ( ( k e. NN /\ x e. CC ) -> 1 e. CC )
63 id 
 |-  ( x e. CC -> x e. CC )
64 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
65 expcl 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( x ^ k ) e. CC )
66 63 64 65 syl2anr 
 |-  ( ( k e. NN /\ x e. CC ) -> ( x ^ k ) e. CC )
67 56 62 66 adddird 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k + 1 ) x. ( x ^ k ) ) = ( ( k x. ( x ^ k ) ) + ( 1 x. ( x ^ k ) ) ) )
68 66 mullidd 
 |-  ( ( k e. NN /\ x e. CC ) -> ( 1 x. ( x ^ k ) ) = ( x ^ k ) )
69 68 oveq2d 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k x. ( x ^ k ) ) + ( 1 x. ( x ^ k ) ) ) = ( ( k x. ( x ^ k ) ) + ( x ^ k ) ) )
70 61 67 69 3eqtrd 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) = ( ( k x. ( x ^ k ) ) + ( x ^ k ) ) )
71 70 mpteq2dva 
 |-  ( k e. NN -> ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) = ( x e. CC |-> ( ( k x. ( x ^ k ) ) + ( x ^ k ) ) ) )
72 cnex 
 |-  CC e. _V
73 72 a1i 
 |-  ( k e. NN -> CC e. _V )
74 56 66 mulcld 
 |-  ( ( k e. NN /\ x e. CC ) -> ( k x. ( x ^ k ) ) e. CC )
75 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
76 expcl 
 |-  ( ( x e. CC /\ ( k - 1 ) e. NN0 ) -> ( x ^ ( k - 1 ) ) e. CC )
77 63 75 76 syl2anr 
 |-  ( ( k e. NN /\ x e. CC ) -> ( x ^ ( k - 1 ) ) e. CC )
78 56 77 mulcld 
 |-  ( ( k e. NN /\ x e. CC ) -> ( k x. ( x ^ ( k - 1 ) ) ) e. CC )
79 simpr 
 |-  ( ( k e. NN /\ x e. CC ) -> x e. CC )
80 eqidd 
 |-  ( k e. NN -> ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) )
81 39 a1i 
 |-  ( k e. NN -> ( _I |` CC ) = ( x e. CC |-> x ) )
82 73 78 79 80 81 offval2 
 |-  ( k e. NN -> ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) = ( x e. CC |-> ( ( k x. ( x ^ ( k - 1 ) ) ) x. x ) ) )
83 56 77 79 mulassd 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k x. ( x ^ ( k - 1 ) ) ) x. x ) = ( k x. ( ( x ^ ( k - 1 ) ) x. x ) ) )
84 expm1t 
 |-  ( ( x e. CC /\ k e. NN ) -> ( x ^ k ) = ( ( x ^ ( k - 1 ) ) x. x ) )
85 84 ancoms 
 |-  ( ( k e. NN /\ x e. CC ) -> ( x ^ k ) = ( ( x ^ ( k - 1 ) ) x. x ) )
86 85 oveq2d 
 |-  ( ( k e. NN /\ x e. CC ) -> ( k x. ( x ^ k ) ) = ( k x. ( ( x ^ ( k - 1 ) ) x. x ) ) )
87 83 86 eqtr4d 
 |-  ( ( k e. NN /\ x e. CC ) -> ( ( k x. ( x ^ ( k - 1 ) ) ) x. x ) = ( k x. ( x ^ k ) ) )
88 87 mpteq2dva 
 |-  ( k e. NN -> ( x e. CC |-> ( ( k x. ( x ^ ( k - 1 ) ) ) x. x ) ) = ( x e. CC |-> ( k x. ( x ^ k ) ) ) )
89 82 88 eqtrd 
 |-  ( k e. NN -> ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) = ( x e. CC |-> ( k x. ( x ^ k ) ) ) )
90 52 50 eqtri 
 |-  ( CC _D ( _I |` CC ) ) = ( x e. CC |-> 1 )
91 90 a1i 
 |-  ( k e. NN -> ( CC _D ( _I |` CC ) ) = ( x e. CC |-> 1 ) )
92 eqidd 
 |-  ( k e. NN -> ( x e. CC |-> ( x ^ k ) ) = ( x e. CC |-> ( x ^ k ) ) )
93 73 62 66 91 92 offval2 
 |-  ( k e. NN -> ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( 1 x. ( x ^ k ) ) ) )
94 68 mpteq2dva 
 |-  ( k e. NN -> ( x e. CC |-> ( 1 x. ( x ^ k ) ) ) = ( x e. CC |-> ( x ^ k ) ) )
95 93 94 eqtrd 
 |-  ( k e. NN -> ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( x ^ k ) ) )
96 73 74 66 89 95 offval2 
 |-  ( k e. NN -> ( ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) = ( x e. CC |-> ( ( k x. ( x ^ k ) ) + ( x ^ k ) ) ) )
97 71 96 eqtr4d 
 |-  ( k e. NN -> ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) = ( ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) )
98 oveq1 
 |-  ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) -> ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) oF x. ( _I |` CC ) ) = ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) )
99 98 oveq1d 
 |-  ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) -> ( ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) = ( ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) )
100 99 eqcomd 
 |-  ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) -> ( ( ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) = ( ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) )
101 97 100 sylan9eq 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) = ( ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) )
102 cnelprrecn 
 |-  CC e. { RR , CC }
103 102 a1i 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> CC e. { RR , CC } )
104 66 fmpttd 
 |-  ( k e. NN -> ( x e. CC |-> ( x ^ k ) ) : CC --> CC )
105 104 adantr 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( x e. CC |-> ( x ^ k ) ) : CC --> CC )
106 f1oi 
 |-  ( _I |` CC ) : CC -1-1-onto-> CC
107 f1of 
 |-  ( ( _I |` CC ) : CC -1-1-onto-> CC -> ( _I |` CC ) : CC --> CC )
108 106 107 mp1i 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( _I |` CC ) : CC --> CC )
109 simpr 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) )
110 109 dmeqd 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> dom ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = dom ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) )
111 78 fmpttd 
 |-  ( k e. NN -> ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) : CC --> CC )
112 111 adantr 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) : CC --> CC )
113 112 fdmd 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> dom ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) = CC )
114 110 113 eqtrd 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> dom ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = CC )
115 1ex 
 |-  1 e. _V
116 115 fconst 
 |-  ( CC X. { 1 } ) : CC --> { 1 }
117 52 feq1i 
 |-  ( ( CC _D ( _I |` CC ) ) : CC --> { 1 } <-> ( CC X. { 1 } ) : CC --> { 1 } )
118 116 117 mpbir 
 |-  ( CC _D ( _I |` CC ) ) : CC --> { 1 }
119 118 fdmi 
 |-  dom ( CC _D ( _I |` CC ) ) = CC
120 119 a1i 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> dom ( CC _D ( _I |` CC ) ) = CC )
121 103 105 108 114 120 dvmulf 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( CC _D ( ( x e. CC |-> ( x ^ k ) ) oF x. ( _I |` CC ) ) ) = ( ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) oF x. ( _I |` CC ) ) oF + ( ( CC _D ( _I |` CC ) ) oF x. ( x e. CC |-> ( x ^ k ) ) ) ) )
122 73 66 79 92 81 offval2 
 |-  ( k e. NN -> ( ( x e. CC |-> ( x ^ k ) ) oF x. ( _I |` CC ) ) = ( x e. CC |-> ( ( x ^ k ) x. x ) ) )
123 expp1 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( x ^ ( k + 1 ) ) = ( ( x ^ k ) x. x ) )
124 63 64 123 syl2anr 
 |-  ( ( k e. NN /\ x e. CC ) -> ( x ^ ( k + 1 ) ) = ( ( x ^ k ) x. x ) )
125 124 mpteq2dva 
 |-  ( k e. NN -> ( x e. CC |-> ( x ^ ( k + 1 ) ) ) = ( x e. CC |-> ( ( x ^ k ) x. x ) ) )
126 122 125 eqtr4d 
 |-  ( k e. NN -> ( ( x e. CC |-> ( x ^ k ) ) oF x. ( _I |` CC ) ) = ( x e. CC |-> ( x ^ ( k + 1 ) ) ) )
127 126 oveq2d 
 |-  ( k e. NN -> ( CC _D ( ( x e. CC |-> ( x ^ k ) ) oF x. ( _I |` CC ) ) ) = ( CC _D ( x e. CC |-> ( x ^ ( k + 1 ) ) ) ) )
128 127 adantr 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( CC _D ( ( x e. CC |-> ( x ^ k ) ) oF x. ( _I |` CC ) ) ) = ( CC _D ( x e. CC |-> ( x ^ ( k + 1 ) ) ) ) )
129 101 121 128 3eqtr2rd 
 |-  ( ( k e. NN /\ ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) ) -> ( CC _D ( x e. CC |-> ( x ^ ( k + 1 ) ) ) ) = ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) )
130 129 ex 
 |-  ( k e. NN -> ( ( CC _D ( x e. CC |-> ( x ^ k ) ) ) = ( x e. CC |-> ( k x. ( x ^ ( k - 1 ) ) ) ) -> ( CC _D ( x e. CC |-> ( x ^ ( k + 1 ) ) ) ) = ( x e. CC |-> ( ( k + 1 ) x. ( x ^ ( ( k + 1 ) - 1 ) ) ) ) ) )
131 9 18 27 36 54 130 nnind 
 |-  ( N e. NN -> ( CC _D ( x e. CC |-> ( x ^ N ) ) ) = ( x e. CC |-> ( N x. ( x ^ ( N - 1 ) ) ) ) )