let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (arccot ^ ))) & Z c= ].(- 1),1.[ & n > 0 holds
( (1 / n) (#) ((#Z n) * (arccot ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 ))) ) )
let Z be open Subset of REAL ; :: thesis: ( Z c= dom ((1 / n) (#) ((#Z n) * (arccot ^ ))) & Z c= ].(- 1),1.[ & n > 0 implies ( (1 / n) (#) ((#Z n) * (arccot ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 ))) ) ) )
assume that
A1:
Z c= dom ((1 / n) (#) ((#Z n) * (arccot ^ )))
and
A2:
Z c= ].(- 1),1.[
and
A3:
n > 0
; :: thesis: ( (1 / n) (#) ((#Z n) * (arccot ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 ))) ) )
A4:
for x being Real st x in Z holds
arccot . x <> 0
proof
let x be
Real;
:: thesis: ( x in Z implies arccot . x <> 0 )
assume A5:
x in Z
;
:: thesis: arccot . x <> 0
assume A6:
arccot . x = 0
;
:: thesis: contradiction
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
then
Z c= [.(- 1),1.]
by A2, XBOOLE_1:1;
then
x in [.(- 1),1.]
by A5;
then
0 in arccot .: [.(- 1),1.]
by A6, SIN_COS9:24, FUNCT_1:def 12;
then A8:
0 in [.(PI / 4),((3 / 4) * PI ).]
by SIN_COS9:56, RELAT_1:148;
PI in ].0 ,4.[
by SIN_COS:def 32;
then
PI > 0
by XXREAL_1:4;
then
PI / 4
> 0 / 4
by XREAL_1:76;
hence
contradiction
by A8, XXREAL_1:1;
:: thesis: verum
end;
A9:
Z c= dom ((#Z n) * (arccot ^ ))
by A1, VALUED_1:def 5;
then
for y being set st y in Z holds
y in dom (arccot ^ )
by FUNCT_1:21;
then A10:
Z c= dom (arccot ^ )
by TARSKI:def 3;
A11:
( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^ ) `| Z) . x = 1 / (((arccot . x) ^2 ) * (1 + (x ^2 ))) ) )
by A2, Th68;
for x being Real st x in Z holds
(#Z n) * (arccot ^ ) is_differentiable_in x
then A12:
(#Z n) * (arccot ^ ) is_differentiable_on Z
by A9, FDIFF_1:16;
for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 )))
proof
let x be
Real;
:: thesis: ( x in Z implies (((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 ))) )
assume A14:
x in Z
;
:: thesis: (((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 )))
then A15:
arccot ^ is_differentiable_in x
by A11, FDIFF_1:16;
A17:
(arccot ^ ) . x = 1
/ (arccot . x)
by A10, A14, RFUNCT_1:def 8;
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x =
(1 / n) * (diff ((#Z n) * (arccot ^ )),x)
by A1, A12, A14, FDIFF_1:28
.=
(1 / n) * ((n * (((arccot ^ ) . x) #Z (n - 1))) * (diff (arccot ^ ),x))
by A15, TAYLOR_1:3
.=
(1 / n) * ((n * (((arccot ^ ) . x) #Z (n - 1))) * (((arccot ^ ) `| Z) . x))
by A11, A14, FDIFF_1:def 8
.=
(1 / n) * ((n * (((arccot ^ ) . x) #Z (n - 1))) * (1 / (((arccot . x) ^2 ) * (1 + (x ^2 )))))
by A2, A14, Th68
.=
(((1 / n) * n) * (((arccot ^ ) . x) #Z (n - 1))) * (1 / (((arccot . x) ^2 ) * (1 + (x ^2 ))))
.=
(1 * (((arccot ^ ) . x) #Z (n - 1))) * (1 / (((arccot . x) ^2 ) * (1 + (x ^2 ))))
by A3, XCMPLX_1:107
.=
((1 / (arccot . x)) #Z (n - 1)) * (1 / (((arccot . x) #Z 2) * (1 + (x ^2 ))))
by A17, FDIFF_7:1
.=
(1 / ((arccot . x) #Z (n - 1))) / (((arccot . x) #Z 2) * (1 + (x ^2 )))
by PREPOWER:52
.=
1
/ (((arccot . x) #Z (n - 1)) * (((arccot . x) #Z 2) * (1 + (x ^2 ))))
by XCMPLX_1:79
.=
1
/ ((((arccot . x) #Z (n - 1)) * ((arccot . x) #Z 2)) * (1 + (x ^2 )))
.=
1
/ (((arccot . x) #Z ((n - 1) + 2)) * (1 + (x ^2 )))
by A4, A14, PREPOWER:54
.=
1
/ (((arccot . x) #Z (n + 1)) * (1 + (x ^2 )))
;
hence
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1
/ (((arccot . x) #Z (n + 1)) * (1 + (x ^2 )))
;
:: thesis: verum
end;
hence
( (1 / n) (#) ((#Z n) * (arccot ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^ ))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2 ))) ) )
by A1, A12, FDIFF_1:28; :: thesis: verum