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