let x be Real; ( x <> 0 implies ( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) ) )
set f = id REAL;
assume A1:
x <> 0
; ( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
( (id REAL) . x = x #Z 1 & x #Z 1 = x |^ 1 )
by Lm2, PREPOWER:36, TAYLOR_1:def 1;
then A2:
(id REAL) . x <> 0
by A1;
A3:
id REAL is_differentiable_in x
by Lm2, TAYLOR_1:2;
then diff (((id REAL) ^),x) =
- ((diff ((id REAL),x)) / (((id REAL) . x) ^2))
by A2, FDIFF_2:15
.=
- ((1 * (x #Z (1 - 1))) / (((id REAL) . xx) ^2))
by Lm2, TAYLOR_1:2
.=
- ((1 * (x #Z 0)) / (x ^2))
.=
- (1 / (x ^2))
by PREPOWER:34
;
hence
( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) )
by A2, A3, FDIFF_2:15; verum