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 object st y in Z holds
y in dom (f1 / (f2 + f1))
by A2, FUNCT_1:11;
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 1;
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 1
.=
(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:12, XREAL_1:8;
A14:
f1 . x =
x #Z 2
by A3, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:36
.=
x ^2
by NEWTON:81
;
then A15:
f1 . x > 0
by A12, SQUARE_1:12;
(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:139;
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:9;
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:36
.=
x ^2
by NEWTON:81
;
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:9;
x <> 0
by A4, A18;
then A20:
1
+ (x ^2) > 0 + 0
by SQUARE_1:12, XREAL_1:8;
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 1
.=
(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:20
.=
(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 7
.=
(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:74
.=
(((1 / 2) * (2 * x)) / ((1 + (x ^2)) ^2)) / ((x ^2) / (1 + (x ^2)))
by XCMPLX_1:74
.=
((x / (1 + (x ^2))) / (1 + (x ^2))) / ((x ^2) / (1 + (x ^2)))
by XCMPLX_1:78
.=
((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:78
.=
(1 / x) / (1 + (x ^2))
by A4, A18, XCMPLX_1:60
.=
1
/ (x * (1 + (x ^2)))
by XCMPLX_1:78
;
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:20; verum