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) )
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;
set g = sin . x;
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 A5: 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
consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (x P_sin )) . m) - (sin . x)) < p by A2, A3, A5, 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 A7: 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
A8: m1 = 2 * j by ABIAN:def 2;
A9: ((n + 1) * 2) / 2 <= (j * 2) / 2 by A7, A8, XREAL_1:74;
n + 1 >= 0 + 1 by XREAL_1:8;
then A10: j - 1 is Element of NAT by A9, NAT_1:20;
(n + 1) - 1 <= j - 1 by A9, XREAL_1:11;
then abs (((Partial_Sums (x P_sin )) . (j - 1)) - (sin . x)) < p by A6, A10;
hence abs (((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . m1) - (sin . x)) < p by A1, A8, A9, 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
A11: m1 = (2 * j) + 1 by ABIAN:9;
A12: (n * 2) + 0 <= (n * 2) + 1 by XREAL_1:8;
((n * 2) + 2) - 1 <= ((2 * j) + 1) - 1 by A7, A11, XREAL_1:11;
then n * 2 <= j * 2 by A12, 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 A6;
hence abs (((Partial_Sums (Maclaurin sin ,].(- r),r.[,x)) . m1) - (sin . x)) < p by A1, A11, 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 A13: 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 A14: lim (Partial_Sums (x P_cos )) = cos . x by SERIES_1:def 3;
A15: Partial_Sums (x P_cos ) is convergent by SIN_COS:39;
set g = cos . x;
A16: 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 A17: 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
consider n being Element of NAT such that
A18: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (x P_cos )) . m) - (cos . x)) < p by A14, A15, A17, 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 A19: 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
A20: m1 = 2 * j by ABIAN:def 2;
(n * 2) + 1 >= n * 2 by XREAL_1:31;
then n * 2 <= j * 2 by A19, A20, 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 A18;
hence abs (((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . m1) - (cos . x)) < p by A1, A20, 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
A21: m1 = (2 * j) + 1 by ABIAN:9;
((n * 2) + 1) - 1 <= ((j * 2) + 1) - 1 by A19, A21, 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 A18;
hence abs (((Partial_Sums (Maclaurin cos ,].(- r),r.[,x)) . m1) - (cos . x)) < p by A1, A21, 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 A16, 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, A13, A16, SEQ_2:def 6, SERIES_1:def 3; :: thesis: verum