let x be Real; :: thesis: for m being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff (#Z m),Z) . m) . x = m !
let m be Element of NAT ; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff (#Z m),Z) . m) . x = m !
let Z be open Subset of REAL ; :: thesis: ( x in Z implies ((diff (#Z m),Z) . m) . x = m ! )
assume A1:
x in Z
; :: thesis: ((diff (#Z m),Z) . m) . x = m !
per cases
( m > 0 or m = 0 )
;
suppose
m > 0
;
:: thesis: ((diff (#Z m),Z) . m) . x = m ! then
0 < 0 + m
;
then
1
<= m
by NAT_1:19;
then reconsider n =
m - 1 as
Element of
NAT by INT_1:18;
A3:
0 + n < n + 1
by XREAL_1:8;
reconsider l =
(n + 1) - n as
Element of
NAT ;
A4:
n ! <> 0
by NEWTON:23;
A6:
#Z 1
is_differentiable_on Z
by Th18, FDIFF_1:34;
then A7:
((n + 1) ! ) (#) (#Z 1) is_differentiable_on Z
by FDIFF_2:19;
Z c= dom (#Z 1)
by A6, FDIFF_1:def 7;
then A8:
Z c= dom (((n + 1) ! ) (#) (#Z 1))
by VALUED_1:def 5;
((diff (#Z m),Z) . m) . x =
(((diff (#Z (n + 1)),Z) . n) `| Z) . x
by TAYLOR_1:def 5
.=
((((((n + 1) choose n) * (n ! )) (#) (#Z ((n + 1) - n))) | Z) `| Z) . x
by Th23, A3
.=
(((((((n + 1) ! ) / ((n ! ) * 1)) * (n ! )) (#) (#Z ((n + 1) - n))) | Z) `| Z) . x
by A3, NEWTON:19, NEWTON:def 3
.=
((((((n + 1) ! ) / 1) (#) (#Z 1)) | Z) `| Z) . x
by A4, XCMPLX_1:93
.=
((((n + 1) ! ) (#) (#Z 1)) `| Z) . x
by A7, FDIFF_2:16
.=
((n + 1) ! ) * (diff (#Z 1),x)
by A8, A1, A6, FDIFF_1:28
.=
((n + 1) ! ) * (1 * (x #Z (1 - 1)))
by TAYLOR_1:2
.=
((n + 1) ! ) * 1
by PREPOWER:44
.=
m !
;
hence
((diff (#Z m),Z) . m) . x = m !
;
:: thesis: verum end;