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 )) ) )
A1: ( (#Z n) . x = x #Z n & x #Z n = x |^ n ) by PREPOWER:46, TAYLOR_1:def 1;
assume x <> 0 ; :: thesis: ( (#Z n) ^ is_differentiable_in x & diff ((#Z n) ^ ),x = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2 )) )
then A2: (#Z n) . x <> 0 by A1, PREPOWER:12;
A3: #Z n is_differentiable_in x by TAYLOR_1:2;
then diff ((#Z n) ^ ),x = - ((diff (#Z n),x) / (((#Z n) . x) ^2 )) by A2, 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 A2, A3, FDIFF_2:15; :: thesis: verum