let x be Real; 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 ; ( 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
; ( (#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; verum