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:36, 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:5;
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