let Z be open Subset of REAL; for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (((#Z 2) * (exp_R - f1)) / exp_R) & ( for x being Real st x in Z holds
( f1 . x = 1 & (exp_R - f1) . x > 0 ) ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1) ) )
let f, f1 be PartFunc of REAL,REAL; ( Z c= dom f & f = ln * (((#Z 2) * (exp_R - f1)) / exp_R) & ( for x being Real st x in Z holds
( f1 . x = 1 & (exp_R - f1) . x > 0 ) ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1) ) ) )
assume that
A1:
Z c= dom f
and
A2:
f = ln * (((#Z 2) * (exp_R - f1)) / exp_R)
and
A3:
for x being Real st x in Z holds
( f1 . x = 1 & (exp_R - f1) . x > 0 )
; ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1) ) )
for y being object st y in Z holds
y in dom (((#Z 2) * (exp_R - f1)) / exp_R)
by A1, A2, FUNCT_1:11;
then A4:
Z c= dom (((#Z 2) * (exp_R - f1)) / exp_R)
by TARSKI:def 3;
then
Z c= (dom ((#Z 2) * (exp_R - f1))) /\ ((dom exp_R) \ (exp_R " {0}))
by RFUNCT_1:def 1;
then A5:
Z c= dom ((#Z 2) * (exp_R - f1))
by XBOOLE_1:18;
then
for y being object st y in Z holds
y in dom (exp_R - f1)
by FUNCT_1:11;
then A6:
Z c= dom (exp_R - f1)
by TARSKI:def 3;
A7:
for x being Real st x in Z holds
(((#Z 2) * (exp_R - f1)) / exp_R) . x > 0
A11:
for x being Real st x in Z holds
f1 . x = 1
by A3;
then A12:
(#Z 2) * (exp_R - f1) is_differentiable_on Z
by A5, Th27;
( exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
exp_R . x <> 0 ) )
by FDIFF_1:26, SIN_COS:54, TAYLOR_1:16;
then A13:
((#Z 2) * (exp_R - f1)) / exp_R is_differentiable_on Z
by A12, FDIFF_2:21;
A14:
for x being Real st x in Z holds
ln * (((#Z 2) * (exp_R - f1)) / exp_R) is_differentiable_in x
then A15:
f is_differentiable_on Z
by A1, A2, FDIFF_1:9;
for x being Real st x in Z holds
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1)
proof
let x be
Real;
( x in Z implies (f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1) )
A16:
exp_R . x > 0
by SIN_COS:54;
A17:
exp_R is_differentiable_in x
by SIN_COS:65;
assume A18:
x in Z
;
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1)
then A19:
(exp_R - f1) . x =
(exp_R . x) - (f1 . x)
by A6, VALUED_1:13
.=
(exp_R . x) - 1
by A3, A18
;
then A20:
(exp_R . x) - 1
> 0
by A3, A18;
A21:
(((#Z 2) * (exp_R - f1)) / exp_R) . x =
(((#Z 2) * (exp_R - f1)) . x) * ((exp_R . x) ")
by A4, A18, RFUNCT_1:def 1
.=
(((#Z 2) * (exp_R - f1)) . x) * (1 / (exp_R . x))
by XCMPLX_1:215
.=
(((#Z 2) * (exp_R - f1)) . x) / (exp_R . x)
by XCMPLX_1:99
.=
((#Z 2) . ((exp_R - f1) . x)) / (exp_R . x)
by A5, A18, FUNCT_1:12
.=
(((exp_R . x) - 1) #Z (1 + 1)) / (exp_R . x)
by A19, TAYLOR_1:def 1
.=
((((exp_R . x) - 1) #Z 1) * (((exp_R . x) - 1) #Z 1)) / (exp_R . x)
by A20, PREPOWER:44
.=
(((exp_R . x) - 1) * (((exp_R . x) - 1) #Z 1)) / (exp_R . x)
by PREPOWER:35
.=
(((exp_R . x) - 1) * ((exp_R . x) - 1)) / (exp_R . x)
by PREPOWER:35
;
A22:
(
((#Z 2) * (exp_R - f1)) / exp_R is_differentiable_in x &
(((#Z 2) * (exp_R - f1)) / exp_R) . x > 0 )
by A13, A7, A18, FDIFF_1:9;
(#Z 2) * (exp_R - f1) is_differentiable_in x
by A12, A18, FDIFF_1:9;
then A23:
diff (
(((#Z 2) * (exp_R - f1)) / exp_R),
x) =
(((diff (((#Z 2) * (exp_R - f1)),x)) * (exp_R . x)) - ((diff (exp_R,x)) * (((#Z 2) * (exp_R - f1)) . x))) / ((exp_R . x) ^2)
by A16, A17, FDIFF_2:14
.=
((((((#Z 2) * (exp_R - f1)) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * (((#Z 2) * (exp_R - f1)) . x))) / ((exp_R . x) ^2)
by A12, A18, FDIFF_1:def 7
.=
((((2 * (exp_R . x)) * ((exp_R . x) - 1)) * (exp_R . x)) - ((diff (exp_R,x)) * (((#Z 2) * (exp_R - f1)) . x))) / ((exp_R . x) ^2)
by A11, A5, A18, Th27
.=
((((2 * (exp_R . x)) * ((exp_R . x) - 1)) * (exp_R . x)) - ((exp_R . x) * (((#Z 2) * (exp_R - f1)) . x))) / ((exp_R . x) ^2)
by SIN_COS:65
.=
((((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((#Z 2) * (exp_R - f1)) . x)) * (exp_R . x)) / ((exp_R . x) * (exp_R . x))
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((#Z 2) * (exp_R - f1)) . x)) / (exp_R . x)
by A16, XCMPLX_1:91
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - ((#Z 2) . ((exp_R - f1) . x))) / (exp_R . x)
by A5, A18, FUNCT_1:12
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((exp_R - f1) . x) #Z 2)) / (exp_R . x)
by TAYLOR_1:def 1
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((exp_R . x) - (f1 . x)) #Z 2)) / (exp_R . x)
by A6, A18, VALUED_1:13
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((exp_R . x) - 1) #Z (1 + 1))) / (exp_R . x)
by A3, A18
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - ((((exp_R . x) - 1) #Z 1) * (((exp_R . x) - 1) #Z 1))) / (exp_R . x)
by A20, PREPOWER:44
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((exp_R . x) - 1) * (((exp_R . x) - 1) #Z 1))) / (exp_R . x)
by PREPOWER:35
.=
(((2 * (exp_R . x)) * ((exp_R . x) - 1)) - (((exp_R . x) - 1) * ((exp_R . x) - 1))) / (exp_R . x)
by PREPOWER:35
.=
(((exp_R . x) + 1) * ((exp_R . x) - 1)) / (exp_R . x)
;
(f `| Z) . x =
diff (
(ln * (((#Z 2) * (exp_R - f1)) / exp_R)),
x)
by A2, A15, A18, FDIFF_1:def 7
.=
((((exp_R . x) + 1) * ((exp_R . x) - 1)) / (exp_R . x)) / ((((exp_R . x) - 1) * ((exp_R . x) - 1)) / (exp_R . x))
by A22, A23, A21, TAYLOR_1:20
.=
(((exp_R . x) + 1) * ((exp_R . x) - 1)) / (((exp_R . x) - 1) * ((exp_R . x) - 1))
by A16, XCMPLX_1:55
.=
((exp_R . x) + 1) / ((exp_R . x) - 1)
by A20, XCMPLX_1:91
;
hence
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1)
;
verum
end;
hence
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1) ) )
by A1, A2, A14, FDIFF_1:9; verum