let r, e be Real; :: thesis: ( 0 < r & 0 < e implies ex n being Nat st
for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e ) )
assume that
A1: r > 0 and
A2: e > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e )
consider r1, r2 being Real such that
A3: ( r1 >= 0 & r2 >= 0 ) and
A4: for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) by A1, Th22;
consider n being Nat such that
A5: for m being Nat st n <= m holds
(r1 * (r2 |^ m)) / (m !) < e by A2, A3, Th12;
take n ; :: thesis: for m being Nat st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e )
let m be Nat; :: thesis: ( n <= m implies for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e ) )
assume n <= m ; :: thesis: for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e )
then A6: (r1 * (r2 |^ m)) / (m !) < e by A5;
let x, s be Real; :: thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies ( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e ) )
assume ( x in ].(- r),r.[ & 0 < s & s < 1 ) ; :: thesis: ( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e )
then ( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| <= (r1 * (r2 |^ m)) / (m !) & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| <= (r1 * (r2 |^ m)) / (m !) ) by A4;
hence ( |.(((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e & |.(((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)).| < e ) by A6, XXREAL_0:2; :: thesis: verum