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