let Z be open Subset of REAL ; for f, f1, f2 being PartFunc of REAL ,REAL st Z c= dom ((1 / 2) (#) f) & f = ln * (f1 / (f2 + f1)) & f1 = #Z 2 & ( for x being Real st x in Z holds
( f2 . x = 1 & x <> 0 ) ) holds
( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 ))) ) )
let f, f1, f2 be PartFunc of REAL ,REAL ; ( Z c= dom ((1 / 2) (#) f) & f = ln * (f1 / (f2 + f1)) & f1 = #Z 2 & ( for x being Real st x in Z holds
( f2 . x = 1 & x <> 0 ) ) implies ( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 ))) ) ) )
assume that
A1:
Z c= dom ((1 / 2) (#) f)
and
A2:
f = ln * (f1 / (f2 + f1))
and
A3:
f1 = #Z 2
and
A4:
for x being Real st x in Z holds
( f2 . x = 1 & x <> 0 )
; ( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 ))) ) )
A5:
Z c= dom f
by A1, VALUED_1:def 5;
then
for y being set st y in Z holds
y in dom (f1 / (f2 + f1))
by A2, FUNCT_1:21;
then A6:
Z c= dom (f1 / (f2 + f1))
by TARSKI:def 3;
then A7:
f1 / (f2 + f1) is_differentiable_on Z
by A3, A4, Th7;
Z c= (dom f1) /\ ((dom (f2 + f1)) \ ((f2 + f1) " {0 }))
by A6, RFUNCT_1:def 4;
then A8:
Z c= dom (f2 + f1)
by XBOOLE_1:1;
A9:
for x being Real st x in Z holds
(f1 / (f1 + f2)) . x > 0
proof
let x be
Real;
( x in Z implies (f1 / (f1 + f2)) . x > 0 )
assume A10:
x in Z
;
(f1 / (f1 + f2)) . x > 0
then A11:
(f1 / (f2 + f1)) . x =
(f1 . x) * (((f2 + f1) . x) " )
by A6, RFUNCT_1:def 4
.=
(f1 . x) / ((f2 + f1) . x)
by XCMPLX_0:def 9
;
A12:
x <> 0
by A4, A10;
then A13:
1
+ (x ^2 ) > 0 + 0
by SQUARE_1:74, XREAL_1:10;
A14:
f1 . x =
x #Z 2
by A3, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:46
.=
x ^2
by NEWTON:100
;
then A15:
f1 . x > 0
by A12, SQUARE_1:74;
(f2 + f1) . x =
(f2 . x) + (f1 . x)
by A8, A10, VALUED_1:def 1
.=
1
+ (x ^2 )
by A4, A10, A14
;
hence
(f1 / (f1 + f2)) . x > 0
by A15, A13, A11, XREAL_1:141;
verum
end;
for x being Real st x in Z holds
ln * (f1 / (f2 + f1)) is_differentiable_in x
then A16:
f is_differentiable_on Z
by A2, A5, FDIFF_1:16;
for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 )))
proof
let x be
Real;
( x in Z implies (((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 ))) )
A17:
f1 . x =
x #Z 2
by A3, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:46
.=
x ^2
by NEWTON:100
;
assume A18:
x in Z
;
(((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 )))
then A19:
(
f1 / (f2 + f1) is_differentiable_in x &
(f1 / (f1 + f2)) . x > 0 )
by A7, A9, FDIFF_1:16;
x <> 0
by A4, A18;
then A20:
1
+ (x ^2 ) > 0 + 0
by SQUARE_1:74, XREAL_1:10;
A21:
(f2 + f1) . x =
(f2 . x) + (f1 . x)
by A8, A18, VALUED_1:def 1
.=
1
+ (x ^2 )
by A4, A18, A17
;
A22:
(f1 / (f2 + f1)) . x =
(f1 . x) * (((f2 + f1) . x) " )
by A6, A18, RFUNCT_1:def 4
.=
(x ^2 ) / (1 + (x ^2 ))
by A17, A21, XCMPLX_0:def 9
;
(((1 / 2) (#) f) `| Z) . x =
(1 / 2) * (diff (ln * (f1 / (f2 + f1))),x)
by A1, A2, A16, A18, FDIFF_1:28
.=
(1 / 2) * ((diff (f1 / (f2 + f1)),x) / ((f1 / (f2 + f1)) . x))
by A19, TAYLOR_1:20
.=
(1 / 2) * ((((f1 / (f2 + f1)) `| Z) . x) / ((f1 / (f2 + f1)) . x))
by A7, A18, FDIFF_1:def 8
.=
(1 / 2) * (((2 * x) / ((1 + (x ^2 )) ^2 )) / ((x ^2 ) / (1 + (x ^2 ))))
by A3, A4, A6, A18, A22, Th7
.=
((1 / 2) * ((2 * x) / ((1 + (x ^2 )) ^2 ))) / ((x ^2 ) / (1 + (x ^2 )))
by XCMPLX_1:75
.=
(((1 / 2) * (2 * x)) / ((1 + (x ^2 )) ^2 )) / ((x ^2 ) / (1 + (x ^2 )))
by XCMPLX_1:75
.=
((x / (1 + (x ^2 ))) / (1 + (x ^2 ))) / ((x ^2 ) / (1 + (x ^2 )))
by XCMPLX_1:79
.=
((x / (1 + (x ^2 ))) / ((x ^2 ) / (1 + (x ^2 )))) / (1 + (x ^2 ))
by XCMPLX_1:48
.=
(x / (x ^2 )) / (1 + (x ^2 ))
by A20, XCMPLX_1:55
.=
((x / x) / x) / (1 + (x ^2 ))
by XCMPLX_1:79
.=
(1 / x) / (1 + (x ^2 ))
by A4, A18, XCMPLX_1:60
.=
1
/ (x * (1 + (x ^2 )))
by XCMPLX_1:79
;
hence
(((1 / 2) (#) f) `| Z) . x = 1
/ (x * (1 + (x ^2 )))
;
verum
end;
hence
( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2 ))) ) )
by A1, A16, FDIFF_1:28; verum