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 & ( 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
A4: 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 A5: 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 )
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 A6: ( 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 )
A7: ( 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 A3, A6;
(r1 * (r2 |^ m)) / (m ! ) < e by A4, A5;
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 A7, XXREAL_0:2; :: thesis: verum