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 () = sin . x by SIN_COS:37;
then A2: lim () = sin . x by SERIES_1:def 3;
A3: Partial_Sums () 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
|.((() . m) - (sin . x)).| < p by ;
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 ;
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 ;
then |.((() . (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 ;
then n * 2 <= j * 2 by XXREAL_0:2;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72;
then |.((() . j) - (sin . x)).| < p by A5;
hence |.(((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)).| < p by ; :: 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 ;
Sum () = cos . x by SIN_COS:37;
then A12: lim () = cos . x by SERIES_1:def 3;
set g = cos . x;
A13: Partial_Sums () 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
|.((() . m) - (cos . x)).| < p by ;
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 ;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72;
then |.((() . j) - (cos . x)).| < p by A15;
hence |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p by ; :: 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 ;
then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72;
then |.((() . j) - (cos . x)).| < p by A15;
hence |.(((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)).| < p by ; :: 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 ;
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 ; :: thesis: verum