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: m ! <> 0 by NEWTON:23;
A4: n ! <> 0 by NEWTON:23;
A5: (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 Th27, A2, A1
.= (((n choose m) * ((x0 #Z (n - m)) * ((x - x0) |^ m))) * (m ! )) / (m ! )
.= ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) by A3, XCMPLX_1:90 ;
(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 Th28, A1
.= (x - x0) |^ n by A4, 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 A5; :: thesis: verum