let Z be open Subset of REAL; :: thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * f)) & f = ((#Z 2) * exp_R) - f1 & ( for x being Real st x in Z holds
( f1 . x = 1 & f . x > 0 ) ) holds
( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) ) )
let f, f1 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom ((1 / 2) (#) (ln * f)) & f = ((#Z 2) * exp_R) - f1 & ( for x being Real st x in Z holds
( f1 . x = 1 & f . x > 0 ) ) implies ( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) ) ) )
assume that
A1: Z c= dom ((1 / 2) (#) (ln * f)) and
A2: f = ((#Z 2) * exp_R) - f1 and
A3: for x being Real st x in Z holds
( f1 . x = 1 & f . x > 0 ) ; :: thesis: ( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) ) )
A4: Z c= dom (ln * f) by A1, VALUED_1:def 5;
then for y being object st y in Z holds
y in dom f by FUNCT_1:11;
then A5: Z c= dom (((#Z 2) * exp_R) - f1) by A2, TARSKI:def 3;
A6: for x being Real st x in Z holds
f1 . x = 1 by A3;
then A7: ((#Z 2) * exp_R) - f1 is_differentiable_on Z by A5, Th25;
for x being Real st x in Z holds
ln * f is_differentiable_in x
proof
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, A3, A7, FDIFF_1:9;
hence ln * f is_differentiable_in x by TAYLOR_1:20; :: thesis: verum
end;
then A8: ln * f is_differentiable_on Z by A4, FDIFF_1:9;
Z c= (dom ((#Z 2) * exp_R)) /\ (dom f1) by A5, VALUED_1:12;
then A9: Z c= dom ((#Z 2) * exp_R) by XBOOLE_1:18;
for x being Real st x in Z holds
(((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x)))
proof
let x be Real; :: thesis: ( x in Z implies (((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) )
A10: exp_R x > 0 by SIN_COS:55;
assume A11: x in Z ; :: thesis: (((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x)))
then A12: ( f is_differentiable_in x & f . x > 0 ) by A2, A3, A7, FDIFF_1:9;
A13: (((#Z 2) * exp_R) - f1) . x = (((#Z 2) * exp_R) . x) - (f1 . x) by A5, A11, VALUED_1:13
.= ((#Z 2) . (exp_R . x)) - (f1 . x) by A9, A11, FUNCT_1:12
.= ((exp_R . x) #Z 2) - (f1 . x) by TAYLOR_1:def 1
.= ((exp_R . x) #Z 2) - 1 by A3, A11
.= ((exp_R x) #Z (1 + 1)) - 1 by SIN_COS:def 23
.= (((exp_R x) #Z 1) * ((exp_R x) #Z 1)) - 1 by A10, PREPOWER:44
.= ((exp_R x) * ((exp_R x) #Z 1)) - 1 by PREPOWER:35
.= ((exp_R x) * (exp_R x)) - 1 by PREPOWER:35 ;
(((1 / 2) (#) (ln * f)) `| Z) . x = (1 / 2) * (diff ((ln * f),x)) by A1, A8, A11, FDIFF_1:20
.= (1 / 2) * ((diff (f,x)) / (f . x)) by A12, TAYLOR_1:20
.= (1 / 2) * ((((((#Z 2) * exp_R) - f1) `| Z) . x) / ((((#Z 2) * exp_R) - f1) . x)) by A2, A7, A11, FDIFF_1:def 7
.= (1 / 2) * ((2 * (exp_R (2 * x))) / (((exp_R x) * (exp_R x)) - 1)) by A6, A5, A11, A13, Th25
.= ((1 / 2) * (2 * (exp_R (2 * x)))) / (((exp_R x) * (exp_R x)) - 1) by XCMPLX_1:74
.= ((exp_R (x + x)) / (exp_R x)) / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) by A10, XCMPLX_1:55
.= (((exp_R x) * (exp_R x)) / (exp_R x)) / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) by SIN_COS:50
.= (((exp_R x) * (exp_R x)) / (exp_R x)) / ((((exp_R x) * (exp_R x)) / (exp_R x)) - (1 / (exp_R x))) by XCMPLX_1:120
.= (exp_R x) / ((((exp_R x) * (exp_R x)) / (exp_R x)) - (1 / (exp_R x))) by A10, XCMPLX_1:89
.= (exp_R x) / ((exp_R x) - (1 / (exp_R x))) by A10, XCMPLX_1:89
.= (exp_R x) / ((exp_R x) - (exp_R (- x))) by TAYLOR_1:4 ;
hence (((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) ; :: thesis: verum
end;
hence ( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) ) ) by A1, A8, FDIFF_1:20; :: thesis: verum