let x be Real; :: thesis: ( x <> 0 implies ( (id REAL ) ^ is_differentiable_in x & diff ((id REAL ) ^ ),x = - (1 / (x ^2 )) ) )
assume A1: x <> 0 ; :: thesis: ( (id REAL ) ^ is_differentiable_in x & diff ((id REAL ) ^ ),x = - (1 / (x ^2 )) )
set f = id REAL ;
A2: (id REAL ) . x = x #Z 1 by Lem5, TAYLOR_1:def 1;
x #Z 1 = x |^ 1 by PREPOWER:46;
then A5: (id REAL ) . x <> 0 by A2, A1, PREPOWER:12;
A6: id REAL is_differentiable_in x by Lem5, TAYLOR_1:2;
diff ((id REAL ) ^ ),x = - ((diff (id REAL ),x) / (((id REAL ) . x) ^2 )) by A5, A6, FDIFF_2:15
.= - ((1 * (x #Z (1 - 1))) / (((id REAL ) . x) ^2 )) by Lem5, TAYLOR_1:2
.= - ((1 * (x #Z 0 )) / (x ^2 )) by FUNCT_1:35
.= - (1 / (x ^2 )) by PREPOWER:44 ;
hence ( (id REAL ) ^ is_differentiable_in x & diff ((id REAL ) ^ ),x = - (1 / (x ^2 )) ) by A6, A5, FDIFF_2:15; :: thesis: verum