let n be Element of NAT ; :: thesis: 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 ; :: thesis: ( not 0 in Z & n >= 1 implies ((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z )
assume A1:
( not 0 in Z & n >= 1 )
; :: thesis: ((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z
A3:
n + 1 >= 1 + 0
by XREAL_1:9;
Z c= REAL \ {0 }
by A1, ZFMISC_1:40;
then A4:
Z c= dom ((#Z (n + 1)) ^ )
by Th36, A3;
(#Z n) ^ is_differentiable_on Z
by A1, Th34;
then A5:
dom (((#Z n) ^ ) `| Z) = Z
by FDIFF_1:def 8;
A6: dom (((- n) (#) ((#Z (n + 1)) ^ )) | Z) =
(dom ((- n) (#) ((#Z (n + 1)) ^ ))) /\ Z
by RELAT_1:90
.=
(dom ((#Z (n + 1)) ^ )) /\ Z
by VALUED_1:def 5
.=
Z
by A4, XBOOLE_1:28
;
for x0 being Real st x0 in Z holds
(((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0
proof
let x0 be
Real;
:: thesis: ( x0 in Z implies (((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0 )
assume A9:
x0 in Z
;
:: thesis: (((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0
A10:
(#Z n) ^ is_differentiable_on Z
by A1, Th34;
A12:
x0 <> 0
by A9, A1;
A14:
dom ((- n) (#) ((#Z (n + 1)) ^ )) = dom ((#Z (n + 1)) ^ )
by VALUED_1:def 5;
A15:
n + 1
>= 1
+ 0
by XREAL_1:9;
Z c= REAL \ {0 }
by A1, ZFMISC_1:40;
then A17:
Z c= dom ((#Z (n + 1)) ^ )
by Th36, A15;
reconsider i =
n - 1 as
Element of
NAT by A1, INT_1:18;
A18:
x0 #Z i <> 0
by A12, PREPOWER:48;
A19:
x0 |^ i <> 0
by A18, PREPOWER:46;
(((#Z n) ^ ) `| Z) . x0 =
diff ((#Z n) ^ ),
x0
by A10, A9, FDIFF_1:def 8
.=
- ((n * (x0 #Z (n - 1))) / ((x0 #Z n) ^2 ))
by Th20, A12
.=
- ((n * (x0 #Z i)) / ((x0 |^ n) ^2 ))
by PREPOWER:46
.=
- ((n * (x0 |^ i)) / ((x0 |^ n) ^2 ))
by PREPOWER:46
.=
- ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i))))
by NEWTON:13
.=
- ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i)))
.=
- ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i)))
by NEWTON:13
.=
- (n / (x0 |^ (i + 2)))
by A19, XCMPLX_1:92
.=
- (n / (x0 #Z (i + 2)))
by PREPOWER:46
.=
- (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 A9, A17, RFUNCT_1:def 8
.=
(- n) * (((#Z (n + 1)) ^ ) . x0)
.=
((- n) (#) ((#Z (n + 1)) ^ )) . x0
by A9, A14, A17, VALUED_1:def 5
.=
(((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0
by A9, FUNCT_1:72
;
hence
(((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0
;
:: thesis: verum
end;
hence
((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z
by A5, A6, PARTFUN1:34; :: thesis: verum