let n, m be Element of NAT ; :: thesis: for r, x being Element of 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 Element of 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 )
|.(0 - 0).| = 0 by ABSVALUE:2;
then A3: 0 in ].(0 - r),(0 + r).[ by A2, RCOMP_1:1;
reconsider s = n - m as Element of NAT by A1, INT_1:5;
A4: n - m > m - m by A1, XREAL_1:9;
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:36
.= ((n choose m) * 0) * (x |^ m) by A4, NEWTON:84
.= 0 ;
hence ( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n ) by A5; :: thesis: verum