let r, x be Real; :: thesis: for m being Element of NAT st 0 < r & m > 0 holds
( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_sin )) . (m - 1) & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_cos )) . m )
let m be Element of NAT ; :: thesis: ( 0 < r & m > 0 implies ( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_sin )) . (m - 1) & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_cos )) . m ) )
assume that
A1: r > 0 and
A2: m > 0 ; :: thesis: ( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_sin )) . (m - 1) & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_cos )) . m )
2 * m > 2 * 0 by A2, XREAL_1:70;
then A3: (2 * m) - 1 is Element of NAT by NAT_1:20;
A4: m - 1 is Element of NAT by A2, NAT_1:20;
A5: (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (2 * m) = ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) - 1)) + ((Maclaurin sin ,].(- r),r.[,x) . (((2 * m) - 1) + 1)) by A3, SERIES_1:def 1
.= ((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * m) - 1)) + 0 by A1, Th20
.= (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . ((2 * (m - 1)) + 1)
.= (Partial_Sums (x P_sin )) . (m - 1) by A1, A4, Th25 ;
(Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) - 1)) + ((Maclaurin cos ,].(- r),r.[,x) . (((2 * m) - 1) + 1)) by A3, SERIES_1:def 1
.= ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * m) - 1)) + ((((- 1) |^ m) * (x |^ (2 * m))) / ((2 * m) ! )) by A1, Th20
.= ((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . ((2 * (m - 1)) + 1)) + ((x P_cos ) . m) by SIN_COS:def 25
.= ((Partial_Sums (x P_cos )) . (m - 1)) + ((x P_cos ) . ((m - 1) + 1)) by A1, A4, Th25
.= (Partial_Sums (x P_cos )) . m by A4, SERIES_1:def 1 ;
hence ( (Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_sin )) . (m - 1) & (Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . (2 * m) = (Partial_Sums (x P_cos )) . m ) by A5; :: thesis: verum