let r, x be Real; :: thesis: ( r > 0 implies ( Partial_Sums (Maclaurin (sin,].(- r),r.[,x)) is convergent & sin . x = Sum (Maclaurin (sin,].(- r),r.[,x)) & Partial_Sums (Maclaurin (cos,].(- r),r.[,x)) is convergent & cos . x = Sum (Maclaurin (cos,].(- r),r.[,x)) ) )
assume A1: r > 0 ; :: thesis: ( Partial_Sums (Maclaurin (sin,].(- r),r.[,x)) is convergent & sin . x = Sum (Maclaurin (sin,].(- r),r.[,x)) & Partial_Sums (Maclaurin (cos,].(- r),r.[,x)) is convergent & cos . x = Sum (Maclaurin (cos,].(- r),r.[,x)) )
set g = sin . x;
Sum (x P_sin) = sin . x by SIN_COS:37;
then A2: lim (Partial_Sums (x P_sin)) = sin . x by SERIES_1:def 3;
A3: Partial_Sums (x P_sin) is convergent by SIN_COS:36;
A4: for p being Real st p > 0 holds
ex n1 being Nat st
for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p

proof

let p be Real; :: thesis: ( p > 0 implies ex n1 being Nat st
for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p )
assume p > 0 ; :: thesis: ex n1 being Nat st
for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p
then consider n being Nat such that
A5: for m being Nat st n <= m holds
|.(((Partial_Sums (x P_sin)) . m) - (sin . x)).| < p by A2, A3, SEQ_2:def 7;
reconsider n1 = (2 * n) + 2 as Nat ;
take n1 ; :: thesis: for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p
let m1 be Nat; :: thesis: ( m1 >= n1 implies |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p )
assume A6: m1 >= n1 ; :: thesis: |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p

per cases ( m1 is even or m1 is odd ) ;

suppose m1 is even ; :: thesis: |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p

then consider j being Nat such that
A7: m1 = 2 * j by ABIAN:def 2;
A8: ((n + 1) * 2) / 2 <= (j * 2) / 2 by A6, A7, XREAL_1:72;
then A9: (n + 1) - 1 <= j - 1 by XREAL_1:9;
n + 1 >= 0 + 1 by XREAL_1:6;
then j - 1 is Element of NAT by A8, NAT_1:20;
then |.(((Partial_Sums (x P_sin)) . (j - 1)) - (sin . x)).| < p by A5, A9;
hence |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p by A1, A7, A8, Th26; :: thesis: verum

end;

suppose m1 is odd ; :: thesis: |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p

then consider j being Nat such that
A10: m1 = (2 * j) + 1 by ABIAN:9;
( (n * 2) + 0 <= (n * 2) + 1 & ((n * 2) + 2) - 1 <= ((2 * j) + 1) - 1 ) by A6, A10, XREAL_1:6, XREAL_1:9;
then n * 2 <= j * 2 by XXREAL_0:2;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72;
then |.(((Partial_Sums (x P_sin)) . j) - (sin . x)).| < p by A5;
hence |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p by A1, A10, Th25; :: thesis: verum

end;

end;

end;

then Partial_Sums (Maclaurin (sin,].(- r),r.[,x)) is convergent by SEQ_2:def 6;
then A11: lim (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) = sin . x by A4, SEQ_2:def 7;
Sum (x P_cos) = cos . x by SIN_COS:37;
then A12: lim (Partial_Sums (x P_cos)) = cos . x by SERIES_1:def 3;
set g = cos . x;
A13: Partial_Sums (x P_cos) is convergent by SIN_COS:36;
A14: for p being Real st p > 0 holds
ex n1 being Nat st
for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p

proof

let p be Real; :: thesis: ( p > 0 implies ex n1 being Nat st
for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p )
assume p > 0 ; :: thesis: ex n1 being Nat st
for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p
then consider n being Nat such that
A15: for m being Nat st n <= m holds
|.(((Partial_Sums (x P_cos)) . m) - (cos . x)).| < p by A12, A13, SEQ_2:def 7;
reconsider n1 = (2 * n) + 1 as Nat ;
take n1 ; :: thesis: for m1 being Nat st m1 >= n1 holds
|.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p
let m1 be Nat; :: thesis: ( m1 >= n1 implies |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p )
assume A16: m1 >= n1 ; :: thesis: |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p

per cases ( m1 is even or m1 is odd ) ;

suppose m1 is even ; :: thesis: |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p

then consider j being Nat such that
A17: m1 = 2 * j by ABIAN:def 2;
(n * 2) + 1 >= n * 2 by XREAL_1:29;
then n * 2 <= j * 2 by A16, A17, XXREAL_0:2;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72;
then |.(((Partial_Sums (x P_cos)) . j) - (cos . x)).| < p by A15;
hence |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p by A1, A17, Th27; :: thesis: verum

end;

suppose m1 is odd ; :: thesis: |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p

then consider j being Nat such that
A18: m1 = (2 * j) + 1 by ABIAN:9;
((n * 2) + 1) - 1 <= ((j * 2) + 1) - 1 by A16, A18, XREAL_1:9;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72;
then |.(((Partial_Sums (x P_cos)) . j) - (cos . x)).| < p by A15;
hence |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p by A1, A18, Th25; :: thesis: verum

end;

end;

end;

then Partial_Sums (Maclaurin (cos,].(- r),r.[,x)) is convergent by SEQ_2:def 6;
then lim (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) = cos . x by A14, SEQ_2:def 7;
hence ( Partial_Sums (Maclaurin (sin,].(- r),r.[,x)) is convergent & sin . x = Sum (Maclaurin (sin,].(- r),r.[,x)) & Partial_Sums (Maclaurin (cos,].(- r),r.[,x)) is convergent & cos . x = Sum (Maclaurin (cos,].(- r),r.[,x)) ) by A4, A11, A14, SEQ_2:def 6, SERIES_1:def 3; :: thesis: verum