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