let Z be open Subset of REAL ; :: thesis: 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 ; :: thesis: ( 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
; :: thesis: ( 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) ) )
for y being set st y in Z holds
y in dom (exp_R / (exp_R + f))
by A1, FUNCT_1:21;
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 4;
then A3:
Z c= dom (exp_R + f)
by XBOOLE_1:1;
then
Z c= (dom exp_R ) /\ (dom f)
by VALUED_1:def 1;
then A4:
Z c= dom f
by XBOOLE_1:18;
A5:
for x being Real st x in Z holds
f . x = (0 * x) + 1
by A2;
then A6:
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
by A4, FDIFF_1:31;
A7:
exp_R is_differentiable_on Z
by FDIFF_1:34, TAYLOR_1:16;
then A8:
( exp_R + f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R + f) `| Z) . x = (diff exp_R ,x) + (diff f,x) ) )
by A3, A6, FDIFF_1:26;
A9:
for x being Real st x in Z holds
((exp_R + f) `| Z) . x = exp_R . x
proof
let x be
Real;
:: thesis: ( x in Z implies ((exp_R + f) `| Z) . x = exp_R . x )
assume A10:
x in Z
;
:: thesis: ((exp_R + f) `| Z) . x = exp_R . x
hence ((exp_R + f) `| Z) . x =
(diff exp_R ,x) + (diff f,x)
by A3, A6, A7, FDIFF_1:26
.=
(exp_R . x) + (diff f,x)
by SIN_COS:70
.=
(exp_R . x) + ((f `| Z) . x)
by A6, A10, FDIFF_1:def 8
.=
(exp_R . x) + 0
by A4, A5, A10, FDIFF_1:31
.=
exp_R . x
;
:: thesis: verum
end;
A11:
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 A13:
exp_R / (exp_R + f) is_differentiable_on Z
by A7, A8, FDIFF_2:21;
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;
:: thesis: ( x in Z implies ((exp_R / (exp_R + f)) `| Z) . x = (exp_R . x) / (((exp_R . x) + 1) ^2 ) )
assume A15:
x in Z
;
:: thesis: ((exp_R / (exp_R + f)) `| Z) . x = (exp_R . x) / (((exp_R . x) + 1) ^2 )
A16:
exp_R is_differentiable_in x
by SIN_COS:70;
A17:
exp_R + f is_differentiable_in x
by A8, A15, FDIFF_1:16;
A18:
(exp_R + f) . x =
(exp_R . x) + (f . x)
by A3, A15, VALUED_1:def 1
.=
(exp_R . x) + 1
by A2, A15
;
then
(
(exp_R + f) . x <> 0 &
(exp_R + f) . x = (exp_R . x) + 1 )
by A11, A15;
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 A16, A17, 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:70
.=
(((exp_R . x) * ((exp_R . x) + 1)) - ((((exp_R + f) `| Z) . x) * (exp_R . x))) / (((exp_R . x) + 1) ^2 )
by A8, A15, A18, FDIFF_1:def 8
.=
(((exp_R . x) * ((exp_R . x) + 1)) - ((exp_R . x) * (exp_R . x))) / (((exp_R . x) + 1) ^2 )
by A9, A15
.=
(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 A13, A15, FDIFF_1:def 8;
:: thesis: verum
end;
A19:
for x being Real st x in Z holds
(exp_R / (exp_R + f)) . x > 0
A23:
for x being Real st x in Z holds
ln * (exp_R / (exp_R + f)) is_differentiable_in x
then A26:
ln * (exp_R / (exp_R + f)) is_differentiable_on Z
by A1, FDIFF_1:16;
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;
:: thesis: ( x in Z implies ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) )
assume A27:
x in Z
;
:: thesis: ((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:21;
then A28:
(exp_R / (exp_R + f)) . x =
(exp_R . x) * (((exp_R + f) . x) " )
by RFUNCT_1:def 4
.=
(exp_R . x) * (1 / ((exp_R + f) . x))
by XCMPLX_1:217
.=
(exp_R . x) / ((exp_R + f) . x)
by XCMPLX_1:100
.=
(exp_R . x) / ((exp_R . x) + (f . x))
by A3, A27, VALUED_1:def 1
.=
(exp_R . x) / ((exp_R . x) + 1)
by A2, A27
;
A29:
exp_R / (exp_R + f) is_differentiable_in x
by A13, A27, FDIFF_1:16;
A30:
(exp_R / (exp_R + f)) . x > 0
by A19, A27;
A31:
(exp_R . x) / ((exp_R . x) + 1) > 0
by A19, A27, A28;
diff (ln * (exp_R / (exp_R + f))),
x =
(diff (exp_R / (exp_R + f)),x) / ((exp_R / (exp_R + f)) . x)
by A29, A30, TAYLOR_1:20
.=
(((exp_R / (exp_R + f)) `| Z) . x) / ((exp_R / (exp_R + f)) . x)
by A13, A27, FDIFF_1:def 8
.=
((exp_R . x) / (((exp_R . x) + 1) ^2 )) / ((exp_R . x) / ((exp_R . x) + 1))
by A14, A27, A28
.=
(((exp_R . x) / ((exp_R . x) + 1)) / ((exp_R . x) + 1)) / ((exp_R . x) / ((exp_R . x) + 1))
by XCMPLX_1:79
.=
(((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 A31, XCMPLX_1:60
;
hence
((ln * (exp_R / (exp_R + f))) `| Z) . x = 1
/ ((exp_R . x) + 1)
by A26, A27, FDIFF_1:def 8;
:: thesis: 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, A23, FDIFF_1:16; :: thesis: verum