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

( 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