let a be Real; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 A1:
( 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 ) )
; :: thesis: ( 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)) ) )
then
for y being set st y in Z holds
y in dom ((f1 + f2) / (f1 - f2))
by FUNCT_1:21;
then A2:
Z c= dom ((f1 + f2) / (f1 - f2))
by TARSKI:def 3;
then A3:
Z c= (dom (f1 + f2)) /\ ((dom (f1 - f2)) \ ((f1 - f2) " {0 }))
by RFUNCT_1:def 4;
then A4:
( Z c= dom (f1 + f2) & Z c= (dom (f1 - f2)) \ ((f1 - f2) " {0 }) )
by XBOOLE_1:18;
A5:
Z c= dom (f1 - f2)
by A3, XBOOLE_1:1;
A6:
( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )
by A1, A2, Th22;
A7:
for x being Real st x in Z holds
((f1 + f2) / (f1 - f2)) . x > 0
A11:
for x being Real st x in Z holds
ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x
then A14:
ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z
by A1, FDIFF_1:16;
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;
:: thesis: ( x in Z implies ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) )
assume A15:
x in Z
;
:: thesis: ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
then A16:
(f1 + f2) / (f1 - f2) is_differentiable_in x
by A6, FDIFF_1:16;
A17:
x in dom ((f1 + f2) / (f1 - f2))
by A1, A15, FUNCT_1:21;
A18:
(
f1 . x = a &
f2 = #Z 2 &
((f1 + f2) / (f1 - f2)) . x > 0 )
by A1, A7, A15;
A19:
(
(f1 - f2) . x <> 0 &
(f1 + f2) . x <> 0 )
by A1, A15;
diff (ln * ((f1 + f2) / (f1 - f2))),
x =
(diff ((f1 + f2) / (f1 - f2)),x) / (((f1 + f2) / (f1 - f2)) . x)
by A16, A18, TAYLOR_1:20
.=
((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) / (f1 - f2)) . x)
by A6, A15, FDIFF_1:def 8
.=
((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))
by A17, RFUNCT_1:def 4
.=
(((4 * a) * x) / (((f1 . x) - (x |^ 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))
by A1, A2, A15, A18, Th22
.=
(((4 * a) * x) / (((f1 . x) - (x #Z 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))
by PREPOWER:46
.=
(((4 * a) * x) / (((f1 . x) - (f2 . x)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))
by A1, TAYLOR_1:def 1
.=
(((4 * a) * x) / (((f1 - f2) . x) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))
by A5, A15, 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:11
.=
(((4 * a) * x) / (((f1 - f2) . x) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x))
by NEWTON:10
.=
((((4 * a) * x) / ((f1 - f2) . x)) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))
by XCMPLX_1:79
.=
((((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 A19, XCMPLX_1:55
.=
((4 * a) * x) / (((f1 + f2) . x) * ((f1 - f2) . x))
by XCMPLX_1:79
.=
((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 - f2) . x))
by A4, A15, VALUED_1:def 1
.=
((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 . x) - (f2 . x)))
by A5, A15, VALUED_1:13
.=
((4 * a) * x) / ((a * a) - ((f2 . x) * (f2 . x)))
by A18
.=
((4 * a) * x) / ((a * a) - ((x #Z 2) * (f2 . x)))
by A1, TAYLOR_1:def 1
.=
((4 * a) * x) / ((a * a) - ((x #Z 2) * (x #Z 2)))
by A1, TAYLOR_1:def 1
.=
((4 * a) * x) / (((a |^ 1) * a) - ((x #Z 2) * (x #Z 2)))
by NEWTON:10
.=
((4 * a) * x) / ((a |^ (1 + 1)) - ((x #Z 2) * (x #Z 2)))
by NEWTON:11
.=
((4 * a) * x) / ((a |^ (1 + 1)) - ((x |^ 2) * (x #Z 2)))
by PREPOWER:46
.=
((4 * a) * x) / ((a |^ 2) - ((x |^ 2) * (x |^ 2)))
by PREPOWER:46
.=
((4 * a) * x) / ((a |^ 2) - (x |^ (2 + 2)))
by NEWTON:13
.=
((4 * a) * x) / ((a |^ 2) - (x |^ 4))
;
hence
((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4))
by A14, A15, FDIFF_1:def 8;
:: thesis: 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, A11, FDIFF_1:16; :: thesis: verum