let x0 be Real; 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 ; 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 ; ( 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
and
A3:
not 0 in Z
; ((diff ((#Z n) ^ ),Z) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0)
A4:
Z c= REAL \ {0 }
by A3, ZFMISC_1:40;
(n + 1) + 1 >= 1 + 0
by XREAL_1:9;
then A5:
Z c= dom ((#Z (n + 2)) ^ )
by A4, Th3;
A6: 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 A5, XBOOLE_1:28
;
A7:
(#Z n) ^ is_differentiable_on Z
by A3, Th43;
A8:
n + 1 >= 1 + 0
by XREAL_1:9;
reconsider m = - n as Element of REAL ;
A9:
(#Z (n + 1)) ^ is_differentiable_on Z
by A3, Th43;
then A10:
m (#) ((#Z (n + 1)) ^ ) is_differentiable_on Z
by FDIFF_2:19;
dom (m (#) ((#Z (n + 1)) ^ )) = dom ((#Z (n + 1)) ^ )
by VALUED_1:def 5;
then A11:
Z c= dom ((- n) (#) ((#Z (n + 1)) ^ ))
by A8, A4, Th3;
((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 A7, FDIFF_2:16
.=
(((m (#) ((#Z (n + 1)) ^ )) | Z) `| Z) . x0
by A1, A3, Th49
.=
((m (#) ((#Z (n + 1)) ^ )) `| Z) . x0
by A10, FDIFF_2:16
.=
m * (diff ((#Z (n + 1)) ^ ),x0)
by A2, A9, A11, FDIFF_1:28
.=
m * ((((#Z (n + 1)) ^ ) `| Z) . x0)
by A2, A9, FDIFF_1:def 8
.=
m * ((((- (n + 1)) (#) ((#Z ((n + 1) + 1)) ^ )) | Z) . x0)
by A3, A8, Th49
.=
m * (((- (n + 1)) (#) (((#Z (n + 2)) ^ ) | Z)) . x0)
by RFUNCT_1:65
.=
m * ((- (n + 1)) * ((((#Z (n + 2)) ^ ) | Z) . x0))
by A2, A6, 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)
; verum