let x0 be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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) ; :: thesis: verum