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