let x0 be Real; :: thesis: for n being Element of NAT
for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds
((diff ((#Z n) ^ ),Z) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0)
let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds
((diff ((#Z n) ^ ),Z) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0)
let Z be open Subset of REAL ; :: thesis: ( n >= 1 & x0 in Z & not 0 in Z implies ((diff ((#Z n) ^ ),Z) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0) )
assume that
A1: n >= 1 and
A2: ( x0 in Z & not 0 in Z ) ; :: thesis: ((diff ((#Z n) ^ ),Z) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0)
A3: (#Z n) ^ is_differentiable_on Z by A2, Th34;
reconsider m = - n as Element of REAL ;
A: (#Z (n + 1)) ^ is_differentiable_on Z by A2, Th34;
then A4: m (#) ((#Z (n + 1)) ^ ) is_differentiable_on Z by FDIFF_2:19;
A5: n + 1 >= 1 + 0 by XREAL_1:9;
A6: dom (m (#) ((#Z (n + 1)) ^ )) = dom ((#Z (n + 1)) ^ ) by VALUED_1:def 5;
B: Z c= REAL \ {0 } by A2, ZFMISC_1:40;
then A7: Z c= dom ((- n) (#) ((#Z (n + 1)) ^ )) by A6, Th36, A5;
(n + 1) + 1 >= 1 + 0 by XREAL_1:9;
then A8: Z c= dom ((#Z (n + 2)) ^ ) by Th36, B;
A9: dom ((- (n + 1)) (#) (((#Z (n + 2)) ^ ) | Z)) = dom (((#Z (n + 2)) ^ ) | Z) by VALUED_1:def 5
.= (dom ((#Z (n + 2)) ^ )) /\ Z by RELAT_1:90
.= Z by A8, XBOOLE_1:28 ;
((diff ((#Z n) ^ ),Z) . 2) . x0 = ((diff ((#Z n) ^ ),Z) . (1 + 1)) . x0
.= (((diff ((#Z n) ^ ),Z) . (1 + 0 )) `| Z) . x0 by TAYLOR_1:def 5
.= ((((diff ((#Z n) ^ ),Z) . 0 ) `| Z) `| Z) . x0 by TAYLOR_1:def 5
.= (((((#Z n) ^ ) | Z) `| Z) `| Z) . x0 by TAYLOR_1:def 5
.= ((((#Z n) ^ ) `| Z) `| Z) . x0 by A3, FDIFF_2:16
.= (((m (#) ((#Z (n + 1)) ^ )) | Z) `| Z) . x0 by Th37, A1, A2
.= ((m (#) ((#Z (n + 1)) ^ )) `| Z) . x0 by A4, FDIFF_2:16
.= m * (diff ((#Z (n + 1)) ^ ),x0) by A2, A, A7, FDIFF_1:28
.= m * ((((#Z (n + 1)) ^ ) `| Z) . x0) by A2, A, FDIFF_1:def 8
.= m * ((((- (n + 1)) (#) ((#Z ((n + 1) + 1)) ^ )) | Z) . x0) by Th37, A5, A2
.= m * (((- (n + 1)) (#) (((#Z (n + 2)) ^ ) | Z)) . x0) by RFUNCT_1:65
.= m * ((- (n + 1)) * ((((#Z (n + 2)) ^ ) | Z) . x0)) by A9, A2, VALUED_1:def 5
.= (n * (n + 1)) * ((((#Z (n + 2)) ^ ) | Z) . x0)
.= (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0) by A2, FUNCT_1:72 ;
hence ((diff ((#Z n) ^ ),Z) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0) ; :: thesis: verum