let x0, x be Real; :: thesis: for n, m being Element of NAT
for Z being open Subset of REAL st x0 in Z & n > m holds
( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
let n, m be Element of NAT ; :: thesis: for Z being open Subset of REAL st x0 in Z & n > m holds
( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
let Z be open Subset of REAL; :: thesis: ( x0 in Z & n > m implies ( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n ) )
assume that
A1: x0 in Z and
A2: n > m ; :: thesis: ( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
A3: n ! <> 0 by NEWTON:17;
A4: (Taylor ((#Z n),Z,x0,x)) . n = ((((diff ((#Z n),Z)) . n) . x0) * ((x - x0) |^ n)) / (n !) by TAYLOR_1:def 7
.= (((x - x0) |^ n) * (n !)) / (n !) by A1, Th37
.= (x - x0) |^ n by A3, XCMPLX_1:89 ;
A5: m ! <> 0 by NEWTON:17;
(Taylor ((#Z n),Z,x0,x)) . m = ((((diff ((#Z n),Z)) . m) . x0) * ((x - x0) |^ m)) / (m !) by TAYLOR_1:def 7
.= ((((n choose m) * (m !)) * (x0 #Z (n - m))) * ((x - x0) |^ m)) / (m !) by A1, A2, Th36
.= (((n choose m) * ((x0 #Z (n - m)) * ((x - x0) |^ m))) * (m !)) / (m !)
.= ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) by A5, XCMPLX_1:89 ;
hence ( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n ) by A4; :: thesis: verum