let a be Real; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) implies ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) )
assume that
A1: Z c= dom (- (ln * f)) and
A2: for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ; :: thesis: ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
now :: thesis: for y being object st y in Z holds
y in dom (ln * f)
let y be object ; :: thesis: ( y in Z implies y in dom (ln * f) )
assume y in Z ; :: thesis: y in dom (ln * f)
then y in dom ((- 1) (#) (ln * f)) by A1;
hence y in dom (ln * f) by VALUED_1:def 5; :: thesis: verum
end;
then A3: Z c= dom (ln * f) by TARSKI:def 3;
then for y being object st y in Z holds
y in dom f by FUNCT_1:11;
then A4: Z c= dom f by TARSKI:def 3;
A5: for x being Real st x in Z holds
f . x = ((- 1) * x) + a
proof
let x be Real; :: thesis: ( x in Z implies f . x = ((- 1) * x) + a )
assume x in Z ; :: thesis: f . x = ((- 1) * x) + a
then f . x = a - x by A2;
hence f . x = ((- 1) * x) + a ; :: thesis: verum
end;
then A6: f is_differentiable_on Z by A4, FDIFF_1:23;
now :: thesis: for x being Real st x in Z holds
ln * f is_differentiable_in x
let x be Real; :: thesis: ( x in Z implies ln * f is_differentiable_in x )
assume x in Z ; :: thesis: ln * f is_differentiable_in x
then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9;
hence ln * f is_differentiable_in x by TAYLOR_1:20; :: thesis: verum
end;
then A7: ln * f is_differentiable_on Z by A3, FDIFF_1:9;
A8: for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x)
proof
let x be Real; :: thesis: ( x in Z implies ((- (ln * f)) `| Z) . x = 1 / (a - x) )
assume A9: x in Z ; :: thesis: ((- (ln * f)) `| Z) . x = 1 / (a - x)
then A10: f . x = a - x by A2;
( f . x > 0 & f is_differentiable_in x ) by A2, A6, A9, FDIFF_1:9;
then diff ((ln * f),x) = (diff (f,x)) / (f . x) by TAYLOR_1:20
.= ((f `| Z) . x) / (f . x) by A6, A9, FDIFF_1:def 7
.= (- 1) / (a - x) by A4, A5, A9, A10, FDIFF_1:23 ;
then (((- 1) (#) (ln * f)) `| Z) . x = (- 1) * ((- 1) / (a - x)) by A1, A7, A9, FDIFF_1:20
.= ((- 1) * (- 1)) / (a - x) by XCMPLX_1:74
.= 1 / (a - x) ;
hence ((- (ln * f)) `| Z) . x = 1 / (a - x) ; :: thesis: verum
end;
Z c= dom ((- 1) (#) (ln * f)) by A1;
hence ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) by A7, A8, FDIFF_1:20; :: thesis: verum