let Z be open Subset of REAL ; :: thesis: ( not 0 in Z implies ((id REAL ) ^ ) `| Z = ((- 1) (#) ((#Z 2) ^ )) | Z )
assume A1:
not 0 in Z
; :: thesis: ((id REAL ) ^ ) `| Z = ((- 1) (#) ((#Z 2) ^ )) | Z
Z1:
dom ((#Z 2) ^ ) = REAL \ {0 }
by Th36;
A2:
Z c= dom ((#Z 2) ^ )
by A1, Z1, ZFMISC_1:40;
(id REAL ) ^ is_differentiable_on Z
by A1, Th34, Lem5;
then A4:
dom (((id REAL ) ^ ) `| Z) = Z
by FDIFF_1:def 8;
A5: dom (((- 1) (#) ((#Z (1 + 1)) ^ )) | Z) =
(dom ((- 1) (#) ((#Z 2) ^ ))) /\ Z
by RELAT_1:90
.=
(dom ((#Z 2) ^ )) /\ Z
by VALUED_1:def 5
.=
Z
by A2, XBOOLE_1:28
;
for x0 being Real st x0 in Z holds
(((id REAL ) ^ ) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^ )) | Z) . x0
proof
let x0 be
Real;
:: thesis: ( x0 in Z implies (((id REAL ) ^ ) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^ )) | Z) . x0 )
assume A8:
x0 in Z
;
:: thesis: (((id REAL ) ^ ) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^ )) | Z) . x0
A9:
(id REAL ) ^ is_differentiable_on Z
by A1, Th34, Lem5;
A11:
x0 <> 0
by A8, A1;
A13:
dom ((- 1) (#) ((#Z 2) ^ )) = dom ((#Z (1 + 1)) ^ )
by VALUED_1:def 5;
(((id REAL ) ^ ) `| Z) . x0 =
diff ((id REAL ) ^ ),
x0
by A9, A8, FDIFF_1:def 8
.=
- (1 / (x0 ^2 ))
by ThA, A11
.=
- (1 / (x0 |^ (1 + 1)))
by NEWTON:100
.=
- (1 / (x0 #Z 2))
by PREPOWER:46
.=
- (1 / ((#Z 2) . x0))
by TAYLOR_1:def 1
.=
- (1 * (((#Z 2) . x0) " ))
by XCMPLX_0:def 9
.=
- (1 * (((#Z 2) ^ ) . x0))
by A8, A2, RFUNCT_1:def 8
.=
(- 1) * (((#Z 2) ^ ) . x0)
.=
((- 1) (#) ((#Z 2) ^ )) . x0
by A8, A2, A13, VALUED_1:def 5
.=
(((- 1) (#) ((#Z 2) ^ )) | Z) . x0
by A8, FUNCT_1:72
;
hence
(((id REAL ) ^ ) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^ )) | Z) . x0
;
:: thesis: verum
end;
hence
((id REAL ) ^ ) `| Z = ((- 1) (#) ((#Z 2) ^ )) | Z
by A5, A4, PARTFUN1:34; :: thesis: verum