let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( (2 / 3) (#) ((#R (3 / 2)) * (f + exp_R )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2)) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) & ( for x being Real st x in Z holds
f . x = 1 ) implies ( (2 / 3) (#) ((#R (3 / 2)) * (f + exp_R )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2)) ) ) )
assume that
A1:
Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R )))
and
A2:
for x being Real st x in Z holds
f . x = 1
; :: thesis: ( (2 / 3) (#) ((#R (3 / 2)) * (f + exp_R )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2)) ) )
A3:
Z c= dom ((#R (3 / 2)) * (f + exp_R ))
by A1, VALUED_1:def 5;
then
for y being set st y in Z holds
y in dom (f + exp_R )
by FUNCT_1:21;
then A4:
Z c= dom (f + exp_R )
by TARSKI:def 3;
then
Z c= (dom exp_R ) /\ (dom f)
by VALUED_1:def 1;
then A5:
Z c= dom f
by XBOOLE_1:18;
A6:
for x being Real st x in Z holds
f . x = (0 * x) + 1
by A2;
then A7:
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
by A5, FDIFF_1:31;
A8:
exp_R is_differentiable_on Z
by FDIFF_1:34, TAYLOR_1:16;
then A9:
f + exp_R is_differentiable_on Z
by A4, A7, FDIFF_1:26;
A10:
for x being Real st x in Z holds
(f + exp_R ) . x > 0
then A14:
(#R (3 / 2)) * (f + exp_R ) is_differentiable_on Z
by A3, FDIFF_1:16;
for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2))
proof
let x be
Real;
:: thesis: ( x in Z implies (((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2)) )
assume A15:
x in Z
;
:: thesis: (((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2))
then A16:
f + exp_R is_differentiable_in x
by A9, FDIFF_1:16;
A17:
(f + exp_R ) . x > 0
by A10, A15;
A18:
(f + exp_R ) . x =
(f . x) + (exp_R . x)
by A4, A15, VALUED_1:def 1
.=
1
+ (exp_R . x)
by A2, A15
;
A19:
((f + exp_R ) `| Z) . x =
(diff f,x) + (diff exp_R ,x)
by A4, A7, A8, A15, FDIFF_1:26
.=
(diff f,x) + (exp_R . x)
by SIN_COS:70
.=
((f `| Z) . x) + (exp_R . x)
by A7, A15, FDIFF_1:def 8
.=
0 + (exp_R . x)
by A5, A6, A15, FDIFF_1:31
.=
exp_R . x
;
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x =
(2 / 3) * (diff ((#R (3 / 2)) * (f + exp_R )),x)
by A1, A14, A15, FDIFF_1:28
.=
(2 / 3) * (((3 / 2) * (((f + exp_R ) . x) #R ((3 / 2) - 1))) * (diff (f + exp_R ),x))
by A16, A17, TAYLOR_1:22
.=
(2 / 3) * (((3 / 2) * (((f + exp_R ) . x) #R ((3 / 2) - 1))) * (((f + exp_R ) `| Z) . x))
by A9, A15, FDIFF_1:def 8
.=
(exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2))
by A18, A19
;
hence
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2))
;
:: thesis: verum
end;
hence
( (2 / 3) (#) ((#R (3 / 2)) * (f + exp_R )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R ))) `| Z) . x = (exp_R . x) * ((1 + (exp_R . x)) #R (1 / 2)) ) )
by A1, A14, FDIFF_1:28; :: thesis: verum