let x0 be Real; for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )
let f be PartFunc of REAL,REAL; ( f is_differentiable_in x0 & f . x0 > 0 implies ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) ) )
assume that
A1:
f is_differentiable_in x0
and
A2:
f . x0 > 0
; ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )
f . x0 in { g where g is Real : 0 < g }
by A2;
then A3:
f . x0 in right_open_halfline 0
by XXREAL_1:230;
then A4:
ln is_differentiable_in f . x0
by Th18, FDIFF_1:9;
thus
ln * f is_differentiable_in x0
by A1, A4, FDIFF_2:13; diff ((ln * f),x0) = (diff (f,x0)) / (f . x0)
thus diff ((ln * f),x0) =
(diff (ln,(f . x0))) * (diff (f,x0))
by A1, A4, FDIFF_2:13
.=
(1 / (f . x0)) * (diff (f,x0))
by A3, Th18
.=
((diff (f,x0)) / (f . x0)) * 1
by XCMPLX_1:75
.=
(diff (f,x0)) / (f . x0)
; verum