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