let a be Real; for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
let Z be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
let f1, f2 be PartFunc of REAL,REAL; ( Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) implies ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) )
assume that
A1:
Z c= dom (ln * ((f1 + f2) / (f1 - f2)))
and
A2:
for x being Real st x in Z holds
f1 . x = a
and
A3:
f2 = #Z 2
and
A4:
for x being Real st x in Z holds
(f1 - f2) . x > 0
and
A5:
for x being Real st x in Z holds
(f1 + f2) . x > 0
; ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
for y being object st y in Z holds
y in dom ((f1 + f2) / (f1 - f2))
by A1, FUNCT_1:11;
then A6:
Z c= dom ((f1 + f2) / (f1 - f2))
;
then A7:
(f1 + f2) / (f1 - f2) is_differentiable_on Z
by A2, A3, A4, Th22;
A8:
Z c= (dom (f1 + f2)) /\ ((dom (f1 - f2)) \ ((f1 - f2) " {0}))
by A6, RFUNCT_1:def 1;
then A9:
Z c= dom (f1 + f2)
by XBOOLE_1:18;
A10:
Z c= dom (f1 - f2)
by A8, XBOOLE_1:1;
A11:
for x being Real st x in Z holds
((f1 + f2) / (f1 - f2)) . x > 0
A14:
for x being Real st x in Z holds
ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x
then A15:
ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
proof
let x be
Real;
( x in Z implies ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) )
assume A16:
x in Z
;
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
then A17:
x in dom ((f1 + f2) / (f1 - f2))
by A1, FUNCT_1:11;
A18:
(f1 - f2) . x <> 0
by A4, A16;
A19:
f1 . x = a
by A2, A16;
(
(f1 + f2) / (f1 - f2) is_differentiable_in x &
((f1 + f2) / (f1 - f2)) . x > 0 )
by A7, A11, A16, FDIFF_1:9;
then diff (
(ln * ((f1 + f2) / (f1 - f2))),
x) =
(diff (((f1 + f2) / (f1 - f2)),x)) / (((f1 + f2) / (f1 - f2)) . x)
by TAYLOR_1:20
.=
((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) / (f1 - f2)) . x)
by A7, A16, FDIFF_1:def 7
.=
((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) . x) * (((f1 - f2) . x) "))
by A17, RFUNCT_1:def 1
.=
(((4 * a) * x) / (((f1 . x) - (x |^ 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) "))
by A2, A3, A4, A6, A16, A19, Th22
.=
(((4 * a) * x) / (((f1 . x) - (x #Z 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) "))
by PREPOWER:36
.=
(((4 * a) * x) / (((f1 . x) - (f2 . x)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) "))
by A3, TAYLOR_1:def 1
.=
(((4 * a) * x) / (((f1 - f2) . x) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) "))
by A10, A16, VALUED_1:13
.=
(((4 * a) * x) / (((f1 - f2) . x) |^ (1 + 1))) / (((f1 + f2) . x) / ((f1 - f2) . x))
by XCMPLX_0:def 9
.=
(((4 * a) * x) / ((((f1 - f2) . x) |^ 1) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x))
by NEWTON:6
.=
(((4 * a) * x) / (((f1 - f2) . x) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x))
.=
((((4 * a) * x) / ((f1 - f2) . x)) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))
by XCMPLX_1:78
.=
((((4 * a) * x) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))) / ((f1 - f2) . x)
by XCMPLX_1:48
.=
(((4 * a) * x) / ((f1 + f2) . x)) / ((f1 - f2) . x)
by A18, XCMPLX_1:55
.=
((4 * a) * x) / (((f1 + f2) . x) * ((f1 - f2) . x))
by XCMPLX_1:78
.=
((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 - f2) . x))
by A9, A16, VALUED_1:def 1
.=
((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 . x) - (f2 . x)))
by A10, A16, VALUED_1:13
.=
((4 * a) * x) / ((a * a) - ((f2 . x) * (f2 . x)))
by A19
.=
((4 * a) * x) / ((a * a) - ((x #Z 2) * (f2 . x)))
by A3, TAYLOR_1:def 1
.=
((4 * a) * x) / ((a * a) - ((x #Z 2) * (x #Z 2)))
by A3, TAYLOR_1:def 1
.=
((4 * a) * x) / (((a |^ 1) * a) - ((x #Z 2) * (x #Z 2)))
.=
((4 * a) * x) / ((a |^ (1 + 1)) - ((x #Z 2) * (x #Z 2)))
by NEWTON:6
.=
((4 * a) * x) / ((a |^ (1 + 1)) - ((x |^ 2) * (x #Z 2)))
by PREPOWER:36
.=
((4 * a) * x) / ((a |^ 2) - ((x |^ 2) * (x |^ 2)))
by PREPOWER:36
.=
((4 * a) * x) / ((a |^ 2) - (x |^ (2 + 2)))
by NEWTON:8
.=
((4 * a) * x) / ((a |^ 2) - (x |^ 4))
;
hence
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
by A15, A16, FDIFF_1:def 7;
verum
end;
hence
( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
by A1, A14, FDIFF_1:9; verum