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 & ( 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))) ) )
A3:
( f = ((#Z 2) * exp_R ) - f1 & ( for x being Real st x in Z holds
f1 . x = 1 ) )
by A2;
A4:
Z c= dom (ln * f)
by A1, VALUED_1:def 5;
then
for y being set st y in Z holds
y in dom f
by FUNCT_1:21;
then A5:
Z c= dom (((#Z 2) * exp_R ) - f1)
by A2, TARSKI:def 3;
then
Z c= (dom ((#Z 2) * exp_R )) /\ (dom f1)
by VALUED_1:12;
then A6:
Z c= dom ((#Z 2) * exp_R )
by XBOOLE_1:18;
A7:
( ((#Z 2) * exp_R ) - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
((((#Z 2) * exp_R ) - f1) `| Z) . x = 2 * (exp_R (2 * x)) ) )
by A3, A5, Th25;
for x being Real st x in Z holds
ln * f is_differentiable_in x
then A10:
ln * f is_differentiable_on Z
by A4, FDIFF_1:16;
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))) )
assume A11:
x in Z
;
:: thesis: (((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x)))
A12:
exp_R x > 0
by SIN_COS:60;
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 A6, A11, FUNCT_1:22
.=
((exp_R . x) #Z 2) - (f1 . x)
by TAYLOR_1:def 1
.=
((exp_R . x) #Z 2) - 1
by A2, A11
.=
((exp_R x) #Z (1 + 1)) - 1
by SIN_COS:def 27
.=
(((exp_R x) #Z 1) * ((exp_R x) #Z 1)) - 1
by A12, PREPOWER:54
.=
((exp_R x) * ((exp_R x) #Z 1)) - 1
by PREPOWER:45
.=
((exp_R x) * (exp_R x)) - 1
by PREPOWER:45
;
A14:
f is_differentiable_in x
by A2, A7, A11, FDIFF_1:16;
A15:
f . x > 0
by A2, A11;
(((1 / 2) (#) (ln * f)) `| Z) . x =
(1 / 2) * (diff (ln * f),x)
by A1, A10, A11, FDIFF_1:28
.=
(1 / 2) * ((diff f,x) / (f . x))
by A14, A15, 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 8
.=
(1 / 2) * ((2 * (exp_R (2 * x))) / (((exp_R x) * (exp_R x)) - 1))
by A3, A5, A11, A13, Th25
.=
((1 / 2) * (2 * (exp_R (2 * x)))) / (((exp_R x) * (exp_R x)) - 1)
by XCMPLX_1:75
.=
((exp_R (x + x)) / (exp_R x)) / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x))
by A12, 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:55
.=
(((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:121
.=
(exp_R x) / ((((exp_R x) * (exp_R x)) / (exp_R x)) - (1 / (exp_R x)))
by A12, XCMPLX_1:90
.=
(exp_R x) / ((exp_R x) - (1 / (exp_R x)))
by A12, XCMPLX_1:90
.=
(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, A10, FDIFF_1:28; :: thesis: verum