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:40;
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:39;
A4: for p being real number st p > 0 holds
ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p

proof

let p be real number ; :: thesis: ( p > 0 implies ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p )
assume p > 0 ; :: thesis: ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p
then consider n being Element of NAT such that
A5: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (x P_sin)) . m) - (sin . x)) < p by A2, A3, SEQ_2:def 7;
set n1 = (2 * n) + 2;
for m1 being Element of NAT st m1 >= (2 * n) + 2 holds
abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p

proof

let m1 be Element of NAT ; :: thesis: ( m1 >= (2 * n) + 2 implies abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p )
assume A6: m1 >= (2 * n) + 2 ; :: thesis: abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p

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

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

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

end;

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

then consider j being Element of 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:8, XREAL_1:11;
then n * 2 <= j * 2 by XXREAL_0:2;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:74;
then abs (((Partial_Sums (x P_sin)) . j) - (sin . x)) < p by A5;
hence abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p by A1, A10, Th25; :: thesis: verum

end;

end;

end;

hence ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p ; :: thesis: verum

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:40;
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:39;
A14: for p being real number st p > 0 holds
ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p

proof

let p be real number ; :: thesis: ( p > 0 implies ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p )
assume p > 0 ; :: thesis: ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p
then consider n being Element of NAT such that
A15: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (x P_cos)) . m) - (cos . x)) < p by A12, A13, SEQ_2:def 7;
set n1 = (2 * n) + 1;
for m1 being Element of NAT st m1 >= (2 * n) + 1 holds
abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p

proof

let m1 be Element of NAT ; :: thesis: ( m1 >= (2 * n) + 1 implies abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p )
assume A16: m1 >= (2 * n) + 1 ; :: thesis: abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p

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

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

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

end;

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

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

end;

end;

end;

hence ex n1 being Element of NAT st
for m1 being Element of NAT st m1 >= n1 holds
abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p ; :: thesis: verum

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