let x be Real; 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 ; 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; ( x in Z implies ((diff ((#Z m),Z)) . m) . x = m ! )
assume A1:
x in Z
; ((diff ((#Z m),Z)) . m) . x = m !
per cases
( m > 0 or m = 0 )
;
suppose
m > 0
;
((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:5;
A2:
0 + n < n + 1
by XREAL_1:6;
A3:
#Z 1
is_differentiable_on Z
by Th8, FDIFF_1:26;
then A4:
((n + 1) !) (#) (#Z 1) is_differentiable_on Z
by FDIFF_2:19;
Z c= dom (#Z 1)
by A3, FDIFF_1:def 6;
then A5:
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 A2, Th32
.=
(((((((n + 1) !) / ((n !) * 1)) * (n !)) (#) (#Z ((n + 1) - n))) | Z) `| Z) . x
by A2, NEWTON:13, NEWTON:def 3
.=
((((((n + 1) !) / 1) (#) (#Z 1)) | Z) `| Z) . x
by XCMPLX_1:92
.=
((((n + 1) !) (#) (#Z 1)) `| Z) . x
by A4, FDIFF_2:16
.=
((n + 1) !) * (diff ((#Z 1),x))
by A1, A3, A5, FDIFF_1:20
.=
((n + 1) !) * (1 * (x #Z (1 - 1)))
by TAYLOR_1:2
.=
((n + 1) !) * 1
by PREPOWER:34
.=
m !
;
hence
((diff ((#Z m),Z)) . m) . x = m !
;
verum end;