let n be Element of NAT ; for Z being open Subset of REAL st not 0 in Z & n >= 1 holds
((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z
let Z be open Subset of REAL; ( not 0 in Z & n >= 1 implies ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z )
assume that
A1:
not 0 in Z
and
A2:
n >= 1
; ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z
( n + 1 >= 1 + 0 & Z c= REAL \ {0} )
by A1, XREAL_1:7, ZFMISC_1:34;
then A3:
Z c= dom ((#Z (n + 1)) ^)
by Th3;
A4:
for x0 being Element of REAL st x0 in Z holds
(((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0
proof
(
n + 1
>= 1
+ 0 &
Z c= REAL \ {0} )
by A1, XREAL_1:7, ZFMISC_1:34;
then A5:
Z c= dom ((#Z (n + 1)) ^)
by Th3;
reconsider i =
n - 1 as
Element of
NAT by A2, INT_1:5;
let x0 be
Element of
REAL ;
( x0 in Z implies (((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0 )
A6:
dom ((- n) (#) ((#Z (n + 1)) ^)) = dom ((#Z (n + 1)) ^)
by VALUED_1:def 5;
assume A7:
x0 in Z
;
(((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0
then
x0 #Z i <> 0
by A1, PREPOWER:38;
then A8:
x0 |^ i <> 0
by PREPOWER:36;
(#Z n) ^ is_differentiable_on Z
by A1, Th43;
then (((#Z n) ^) `| Z) . x0 =
diff (
((#Z n) ^),
x0)
by A7, FDIFF_1:def 7
.=
- ((n * (x0 #Z (n - 1))) / ((x0 #Z n) ^2))
by A1, A7, Th29
.=
- ((n * (x0 #Z i)) / ((x0 |^ n) ^2))
by PREPOWER:36
.=
- ((n * (x0 |^ i)) / ((x0 |^ n) ^2))
by PREPOWER:36
.=
- ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i))))
by NEWTON:8
.=
- ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i)))
.=
- ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i)))
by NEWTON:8
.=
- (n / (x0 |^ (i + 2)))
by A8, XCMPLX_1:91
.=
- (n / (x0 #Z (i + 2)))
by PREPOWER:36
.=
- (n / ((#Z (i + 2)) . x0))
by TAYLOR_1:def 1
.=
- (n * (((#Z (n + 1)) . x0) "))
by XCMPLX_0:def 9
.=
- (n * (((#Z (n + 1)) ^) . x0))
by A7, A5, RFUNCT_1:def 2
.=
(- n) * (((#Z (n + 1)) ^) . x0)
.=
((- n) (#) ((#Z (n + 1)) ^)) . x0
by A7, A6, A5, VALUED_1:def 5
.=
(((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0
by A7, FUNCT_1:49
;
hence
(((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0
;
verum
end;
(#Z n) ^ is_differentiable_on Z
by A1, Th43;
then A9:
dom (((#Z n) ^) `| Z) = Z
by FDIFF_1:def 7;
dom (((- n) (#) ((#Z (n + 1)) ^)) | Z) =
(dom ((- n) (#) ((#Z (n + 1)) ^))) /\ Z
by RELAT_1:61
.=
(dom ((#Z (n + 1)) ^)) /\ Z
by VALUED_1:def 5
.=
Z
by A3, XBOOLE_1:28
;
hence
((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z
by A9, A4, PARTFUN1:5; verum