let n, m be Element of NAT ; :: thesis: for r, x being Real st n > m & r > 0 holds
( (Maclaurin (#Z n),].(- r),r.[,x) . m = 0 & (Maclaurin (#Z n),].(- r),r.[,x) . n = x |^ n )
let r, x be Real; :: thesis: ( n > m & r > 0 implies ( (Maclaurin (#Z n),].(- r),r.[,x) . m = 0 & (Maclaurin (#Z n),].(- r),r.[,x) . n = x |^ n ) )
assume that
A1: n > m and
A2: r > 0 ; :: thesis: ( (Maclaurin (#Z n),].(- r),r.[,x) . m = 0 & (Maclaurin (#Z n),].(- r),r.[,x) . n = x |^ n )
abs (0 - 0 ) = 0 by ABSVALUE:7;
then A3: 0 in ].(0 - r),(0 + r).[ by A2, RCOMP_1:8;
reconsider s = n - m as Element of NAT by A1, INT_1:18;
A4: n - m > m - m by A1, XREAL_1:11;
A5: (Maclaurin (#Z n),].(- r),r.[,x) . n = (Taylor (#Z n),].(- r),r.[,0 ,x) . n by TAYLOR_2:def 1
.= (x - 0 ) |^ n by A1, A3, Th41
.= x |^ n ;
(Maclaurin (#Z n),].(- r),r.[,x) . m = (Taylor (#Z n),].(- r),r.[,0 ,x) . m by TAYLOR_2:def 1
.= ((n choose m) * (0 #Z (n - m))) * ((x - 0 ) |^ m) by A1, A3, Th41
.= ((n choose m) * (0 |^ s)) * (x |^ m) by PREPOWER:46
.= ((n choose m) * 0 ) * (x |^ m) by A4, NEWTON:103
.= 0 ;
hence ( (Maclaurin (#Z n),].(- r),r.[,x) . m = 0 & (Maclaurin (#Z n),].(- r),r.[,x) . n = x |^ n ) by A5; :: thesis: verum