let Z be open Subset of REAL; ( Z c= dom ((id Z) (#) ln) implies ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) )
set f = ln ;
assume A1:
Z c= dom ((id Z) (#) ln)
; ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) )
then A2:
Z c= (dom (id Z)) /\ (dom ln)
by VALUED_1:def 4;
then A3:
Z c= dom (id Z)
by XBOOLE_1:18;
A4:
for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0
by FUNCT_1:18;
then A5:
id Z is_differentiable_on Z
by A3, FDIFF_1:23;
A6:
Z c= dom ln
by A2, XBOOLE_1:18;
then A7:
ln is_differentiable_on Z
by Th19;
for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x)
proof
let x be
Real;
( x in Z implies (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) )
assume A8:
x in Z
;
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x)
then A9:
x <> 0
by A6, TAYLOR_1:18, XXREAL_1:4;
(((id Z) (#) ln) `| Z) . x =
(((id Z) . x) * (diff (ln,x))) + ((ln . x) * (diff ((id Z),x)))
by A1, A5, A7, A8, FDIFF_1:21
.=
(((id Z) . x) * ((ln `| Z) . x)) + ((ln . x) * (diff ((id Z),x)))
by A7, A8, FDIFF_1:def 7
.=
(((id Z) . x) * (1 / x)) + ((ln . x) * (diff ((id Z),x)))
by A6, A8, Th19
.=
(x * (1 / x)) + ((ln . x) * (diff ((id Z),x)))
by A8, FUNCT_1:18
.=
(x * (1 / x)) + ((ln . x) * (((id Z) `| Z) . x))
by A5, A8, FDIFF_1:def 7
.=
(x * (1 / x)) + ((ln . x) * 1)
by A3, A4, A8, FDIFF_1:23
.=
1
+ (ln . x)
by A9, XCMPLX_1:106
;
hence
(((id Z) (#) ln) `| Z) . x = 1
+ (ln . x)
;
verum
end;
hence
( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) )
by A1, A5, A7, FDIFF_1:21; verum