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