let a be Real; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 )
; :: thesis: ( 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) & Z c= (dom (f1 - f2)) \ ((f1 - f2) " {0 }) )
by XBOOLE_1:18;
A8:
Z c= dom (f1 - f2)
by A6, XBOOLE_1:1;
A9:
for x being Real st x in Z holds
( f1 . x = a ^2 & (f1 - f2) . x <> 0 )
by A4;
then A10:
( (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 ^2 )) * x) / (((a ^2 ) - (x |^ 2)) ^2 ) ) )
by A3, A5, Th4;
A11:
for x being Real st x in Z holds
((f1 + f2) / (f1 - f2)) . x > 0
proof
let x be
Real;
:: thesis: ( x in Z implies ((f1 + f2) / (f1 - f2)) . x > 0 )
assume A12:
x in Z
;
:: thesis: ((f1 + f2) / (f1 - f2)) . x > 0
then A13:
(f1 - f2) . x > 0
by A4;
A14:
f2 . x =
x #Z 2
by A3, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:46
;
A15:
(f1 + f2) . x =
(f1 . x) + (f2 . x)
by A7, A12, VALUED_1:def 1
.=
(a ^2 ) + (x |^ 2)
by A4, A12, A14
;
a <> 0
by A4, A12;
then A16:
a ^2 > 0
by SQUARE_1:74;
x |^ 2
= x ^2
by NEWTON:100;
then A17:
(a ^2 ) + (x |^ 2) > 0 + 0
by A16, XREAL_1:10, XREAL_1:65;
((f1 + f2) / (f1 - f2)) . x =
((f1 + f2) . x) * (((f1 - f2) . x) " )
by A5, A12, RFUNCT_1:def 4
.=
((f1 + f2) . x) / ((f1 - f2) . x)
by XCMPLX_0:def 9
;
hence
((f1 + f2) / (f1 - f2)) . x > 0
by A13, A15, A17, XREAL_1:141;
:: thesis: verum
end;
A18:
for x being Real st x in Z holds
ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x
then A21:
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;
:: thesis: ( x in Z implies (f `| Z) . x = ((4 * (a ^2 )) * x) / ((a |^ 4) - (x |^ 4)) )
assume A22:
x in Z
;
:: thesis: (f `| Z) . x = ((4 * (a ^2 )) * x) / ((a |^ 4) - (x |^ 4))
then A23:
(f1 + f2) / (f1 - f2) is_differentiable_in x
by A10, FDIFF_1:16;
A24:
f2 . x =
x #Z 2
by A3, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:46
;
A25:
(f1 + f2) . x =
(f1 . x) + (f2 . x)
by A7, A22, VALUED_1:def 1
.=
(a ^2 ) + (x |^ 2)
by A4, A22, A24
;
A26:
(f1 - f2) . x =
(f1 . x) - (f2 . x)
by A8, A22, VALUED_1:13
.=
(a ^2 ) - (x |^ 2)
by A4, A22, A24
;
A27:
((f1 + f2) / (f1 - f2)) . x =
((f1 + f2) . x) * (((f1 - f2) . x) " )
by A5, A22, RFUNCT_1:def 4
.=
((a ^2 ) + (x |^ 2)) / ((a ^2 ) - (x |^ 2))
by A25, A26, XCMPLX_0:def 9
;
A28:
(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
;
A29:
(x |^ 2) ^2 =
(x |^ 2) |^ 2
by WSIERP_1:2
.=
x |^ (2 * 2)
by NEWTON:14
.=
x |^ 4
;
A30:
(a ^2 ) - (x |^ 2) > 0
by A4, A22, A26;
((f1 + f2) / (f1 - f2)) . x > 0
by A11, A22;
then diff (ln * ((f1 + f2) / (f1 - f2))),
x =
(diff ((f1 + f2) / (f1 - f2)),x) / (((f1 + f2) / (f1 - f2)) . x)
by A23, TAYLOR_1:20
.=
((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) / (f1 - f2)) . x)
by A10, A22, FDIFF_1:def 8
.=
(((4 * (a ^2 )) * x) / (((a ^2 ) - (x |^ 2)) ^2 )) / (((a ^2 ) + (x |^ 2)) / ((a ^2 ) - (x |^ 2)))
by A3, A5, A9, A22, 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 A30, 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 A28, A29
;
hence
(f `| Z) . x = ((4 * (a ^2 )) * x) / ((a |^ 4) - (x |^ 4))
by A2, A21, A22, FDIFF_1:def 8;
:: thesis: 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; :: thesis: verum