let Z be open Subset of REAL ; :: thesis: for g being PartFunc of REAL ,REAL st not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^ ))) & g = #Z 2 & ( for x being Real st x in Z holds
( ((id Z) ^ ) . x > - 1 & ((id Z) ^ ) . x < 1 ) ) holds
( g (#) (arctan * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 ))) ) )
let g be PartFunc of REAL ,REAL ; :: thesis: ( not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^ ))) & g = #Z 2 & ( for x being Real st x in Z holds
( ((id Z) ^ ) . x > - 1 & ((id Z) ^ ) . x < 1 ) ) implies ( g (#) (arctan * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 ))) ) ) )
set f = id Z;
assume that
A1:
( not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^ ))) )
and
A2:
g = #Z 2
and
A3:
for x being Real st x in Z holds
( ((id Z) ^ ) . x > - 1 & ((id Z) ^ ) . x < 1 )
; :: thesis: ( g (#) (arctan * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 ))) ) )
Z c= (dom g) /\ (dom (arctan * ((id Z) ^ )))
by A1, VALUED_1:def 4;
then A4:
( Z c= dom g & Z c= dom (arctan * ((id Z) ^ )) )
by XBOOLE_1:18;
then
for y being set st y in Z holds
y in dom ((id Z) ^ )
by FUNCT_1:21;
then A5:
Z c= dom ((id Z) ^ )
by TARSKI:def 3;
A6:
( arctan * ((id Z) ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan * ((id Z) ^ )) `| Z) . x = - (1 / (1 + (x ^2 ))) ) )
by A3, A4, SIN_COS9:111, A1;
for x being Real st x in Z holds
g is_differentiable_in x
by A2, TAYLOR_1:2;
then A7:
g is_differentiable_on Z
by A4, FDIFF_1:16;
A8:
for x being Real st x in Z holds
(g `| Z) . x = 2 * x
for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 )))
proof
let x be
Real;
:: thesis: ( x in Z implies ((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 ))) )
assume A11:
x in Z
;
:: thesis: ((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 )))
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x =
(((arctan * ((id Z) ^ )) . x) * (diff g,x)) + ((g . x) * (diff (arctan * ((id Z) ^ )),x))
by A1, A6, A7, A11, FDIFF_1:29
.=
(((arctan * ((id Z) ^ )) . x) * ((g `| Z) . x)) + ((g . x) * (diff (arctan * ((id Z) ^ )),x))
by A7, A11, FDIFF_1:def 8
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + ((g . x) * (diff (arctan * ((id Z) ^ )),x))
by A8, A11
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + ((x #Z 2) * (diff (arctan * ((id Z) ^ )),x))
by A2, TAYLOR_1:def 1
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + ((x #Z 2) * (((arctan * ((id Z) ^ )) `| Z) . x))
by A6, A11, FDIFF_1:def 8
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + ((x #Z (1 + 1)) * (- (1 / (1 + (x ^2 )))))
by A3, A4, A11, SIN_COS9:111, A1
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * (- (1 / (1 + (x ^2 )))))
by TAYLOR_1:1
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + ((x * (x #Z 1)) * (- (1 / (1 + (x ^2 )))))
by PREPOWER:45
.=
(((arctan * ((id Z) ^ )) . x) * (2 * x)) + ((x ^2 ) * (- (1 / (1 + (x ^2 )))))
by PREPOWER:45
.=
((arctan . (((id Z) ^ ) . x)) * (2 * x)) - ((x ^2 ) / (1 + (x ^2 )))
by A4, A11, FUNCT_1:22
.=
((arctan . (((id Z) . x) " )) * (2 * x)) - ((x ^2 ) / (1 + (x ^2 )))
by A5, A11, RFUNCT_1:def 8
.=
((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 )))
by A11, FUNCT_1:35
;
hence
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 )))
;
:: thesis: verum
end;
hence
( g (#) (arctan * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^ ))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2 ) / (1 + (x ^2 ))) ) )
by A1, A6, A7, FDIFF_1:29; :: thesis: verum