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:34;
(n + 1) + 1 >= 1 + 0
by XREAL_1:7;
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:61
.=
Z
by A5, XBOOLE_1:28
;
A7:
(#Z n) ^ is_differentiable_on Z
by A3, Th43;
A8:
n + 1 >= 1 + 0
by XREAL_1:7;
reconsider m = - n as Element of REAL by XREAL_0:def 1;
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:20
.=
m * ((((#Z (n + 1)) ^) `| Z) . x0)
by A2, A9, FDIFF_1:def 7
.=
m * ((((- (n + 1)) (#) ((#Z ((n + 1) + 1)) ^)) | Z) . x0)
by A3, A8, Th49
.=
m * (((- (n + 1)) (#) (((#Z (n + 2)) ^) | Z)) . x0)
by RFUNCT_1:49
.=
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:49
;
hence
((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0)
; verum