let x be Real; :: thesis: for n being Element of NAT st x <> 0 holds
( (#Z n) ^ is_differentiable_in x & diff ((#Z n) ^ ),x = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )) )
let n be Element of NAT ; :: thesis: ( x <> 0 implies ( (#Z n) ^ is_differentiable_in x & diff ((#Z n) ^ ),x = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )) ) )
assume A1: x <> 0 ; :: thesis: ( (#Z n) ^ is_differentiable_in x & diff ((#Z n) ^ ),x = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )) )
A2: (#Z n) . x = x #Z n by TAYLOR_1:def 1;
A3: x #Z n = x |^ n by PREPOWER:46;
A5: (#Z n) . x <> 0 by A2, A3, A1, PREPOWER:12;
A6: #Z n is_differentiable_in x by TAYLOR_1:2;
diff ((#Z n) ^ ),x = - ((diff (#Z n),x) / (((#Z n) . x) ^2 )) by A5, A6, FDIFF_2:15
.= - ((n * (x #Z (n - 1))) / (((#Z n) . x) ^2 )) by TAYLOR_1:2
.= - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )) by TAYLOR_1:def 1 ;
hence ( (#Z n) ^ is_differentiable_in x & diff ((#Z n) ^ ),x = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )) ) by A5, A6, FDIFF_2:15; :: thesis: verum