let Z be open Subset of REAL; ( not 0 in Z & Z c= dom (ln * ((id Z) ^)) implies ( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) ) )
set f = id Z;
assume that
A1:
not 0 in Z
and
A2:
Z c= dom (ln * ((id Z) ^))
; ( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) )
dom (ln * ((id Z) ^)) c= dom ((id Z) ^)
by RELAT_1:25;
then A3:
Z c= dom ((id Z) ^)
by A2, XBOOLE_1:1;
A4:
for x being Real st x in Z holds
((id Z) ^) . x > 0
A7:
for x being Real st x in Z holds
(id Z) . x > 0
A9:
(id Z) ^ is_differentiable_on Z
by A1, FDIFF_5:4;
A10:
for x being Real st x in Z holds
( ln * ((id Z) ^) is_differentiable_in x & diff ((ln * ((id Z) ^)),x) = (diff (((id Z) ^),x)) / (((id Z) ^) . x) )
then A11:
for x being Real st x in Z holds
ln * ((id Z) ^) is_differentiable_in x
;
then A12:
ln * ((id Z) ^) is_differentiable_on Z
by A2, FDIFF_1:9;
for x being Real st x in Z holds
((ln * ((id Z) ^)) `| Z) . x = - (1 / x)
proof
let x be
Real;
( x in Z implies ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) )
assume A13:
x in Z
;
((ln * ((id Z) ^)) `| Z) . x = - (1 / x)
then
(id Z) . x <> 0
by A7;
then A14:
x <> 0
by A13, FUNCT_1:18;
diff (
(ln * ((id Z) ^)),
x) =
(diff (((id Z) ^),x)) / (((id Z) ^) . x)
by A10, A13
.=
((((id Z) ^) `| Z) . x) / (((id Z) ^) . x)
by A9, A13, FDIFF_1:def 7
.=
((((id Z) ^) `| Z) . x) / (((id Z) . x) ")
by A3, A13, RFUNCT_1:def 2
.=
((((id Z) ^) `| Z) . x) / (1 * (x "))
by A13, FUNCT_1:18
.=
(- (1 / (x ^2))) / (1 * (x "))
by A1, A13, FDIFF_5:4
.=
- (x / (x ^2))
.=
- ((x / x) / x)
by XCMPLX_1:78
.=
- (1 / x)
by A14, XCMPLX_1:60
;
hence
((ln * ((id Z) ^)) `| Z) . x = - (1 / x)
by A12, A13, FDIFF_1:def 7;
verum
end;
hence
( ln * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((id Z) ^)) `| Z) . x = - (1 / x) ) )
by A2, A11, FDIFF_1:9; verum