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:23;
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:90 ;
A5: m ! <> 0 by NEWTON:23;
(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:90 ;
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