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