let x be Real; :: thesis: ( x <> 0 implies ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) ) )
A1: ( (#Z 2) . x = x #Z 2 & x #Z 2 = x |^ 2 ) by PREPOWER:36, TAYLOR_1:def 1;
assume x <> 0 ; :: thesis: ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) )
then A2: (#Z 2) . x <> 0 by A1, PREPOWER:5;
A3: #Z 2 is_differentiable_in x by TAYLOR_1:2;
then diff (((#Z 2) ^),x) = - ((diff ((#Z 2),x)) / (((#Z 2) . x) ^2)) by A2, FDIFF_2:15
.= - ((2 * (x #Z (2 - 1))) / (((#Z 2) . x) ^2)) by TAYLOR_1:2
.= - ((2 * (x #Z 1)) / ((x #Z 2) ^2)) by TAYLOR_1:def 1
.= - ((2 * x) / ((x #Z 2) ^2)) by PREPOWER:35 ;
hence ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) ) by A2, A3, FDIFF_2:15; :: thesis: verum