let r be Real; :: thesis: ( 0 < r implies ex M, L being Real st
( 0 <= M & 0 <= L & ( 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 !) ) ) )
assume A1: r > 0 ; :: thesis: ex M, L being Real st
( 0 <= M & 0 <= L & ( 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 !) ) )
take M = exp_R . r; :: thesis: ex L being Real st
( 0 <= M & 0 <= L & ( 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 !) ) )
take L = r; :: thesis: ( 0 <= M & 0 <= L & ( 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 !) ) )

now

let n be Element of NAT ; :: thesis: 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 !)

now

A2: for a, b being Real st 0 <= a & a <= b holds
for n being Element of NAT holds
( 0 <= a |^ n & a |^ n <= b |^ n )

proof

let a, b be Real; :: thesis: ( 0 <= a & a <= b implies for n being Element of NAT holds
( 0 <= a |^ n & a |^ n <= b |^ n ) )
assume that
A3: 0 <= a and
A4: a <= b ; :: thesis: for n being Element of NAT holds
( 0 <= a |^ n & a |^ n <= b |^ n )
defpred S₁[ Element of NAT ] means ( 0 <= a |^ $1 & a |^ $1 <= b |^ $1 );
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
0 * a <= (a |^ k) * a by A3, A6;
hence a |^ (k + 1) >= 0 by NEWTON:6; :: thesis: a |^ (k + 1) <= b |^ (k + 1)
( b |^ (k + 1) = (b |^ k) * b & (a |^ k) * a <= (b |^ k) * b ) by A3, A4, A6, NEWTON:6, XREAL_1:66;
hence a |^ (k + 1) <= b |^ (k + 1) by NEWTON:6; :: thesis: verum

end;

b |^ 0 = 1 by NEWTON:4;
then A7: S₁[ 0 ] by NEWTON:4;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A5);
hence for n being Element of NAT holds
( 0 <= a |^ n & a |^ n <= b |^ n ) ; :: thesis: verum

end;

let x, s be Real; :: thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) )
assume that
A8: x in ].(- r),r.[ and
A9: 0 < s and
A10: s < 1 ; :: thesis: abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !)
x in ].(0 - r),(0 + r).[ by A8;
then A11: abs (x - 0) < r by RCOMP_1:1;
abs x >= 0 by COMPLEX1:46;
then A12: (abs x) |^ n <= L |^ n by A11, A2;
A13: n ! > 0 by NEWTON:17;
abs x >= 0 by COMPLEX1:46;
then s * (abs x) < 1 * r by A9, A10, A11, XREAL_1:97;
then (abs s) * (abs x) < r by A9, ABSVALUE:def 1;
then abs ((s * x) - 0) < r by COMPLEX1:65;
then A14: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:1;
then A15: abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) = abs (((exp_R . (s * x)) * (x |^ n)) / (n !)) by Th7
.= abs ((exp_R . (s * x)) * ((x |^ n) / (n !))) by XCMPLX_1:74
.= (abs (exp_R . (s * x))) * (abs ((x |^ n) / (n !))) by COMPLEX1:65 ;
exp_R . (s * x) >= 0 by SIN_COS:54;
then A16: ( r in ([#] REAL) /\ (dom exp_R) & abs (exp_R . (s * x)) = exp_R . (s * x) ) by ABSVALUE:def 1, TAYLOR_1:16;
for x0 being Real holds 0 <= diff (exp_R,x0) by TAYLOR_1:16;
then A17: exp_R | ([#] REAL) is non-decreasing by FDIFF_2:39, TAYLOR_1:16;
abs ((x |^ n) / (n !)) = (abs (x |^ n)) / (abs (n !)) by COMPLEX1:67
.= (abs (x |^ n)) / (n !) by A13, ABSVALUE:def 1
.= ((abs x) |^ n) / (n !) by Th1 ;
then A18: abs ((x |^ n) / (n !)) <= (L |^ n) / (n !) by A13, A12, XREAL_1:72;
A19: ( abs (exp_R . (s * x)) >= 0 & abs ((x |^ n) / (n !)) >= 0 ) by COMPLEX1:46;
s * x in { p where p is Real : ( - r < p & p < r ) } by A14, RCOMP_1:def 2;
then ex g being Real st
( g = s * x & - r < g & g < r ) ;
then abs (exp_R . (s * x)) <= M by A17, A16, RFUNCT_2:24, TAYLOR_1:16;
then abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= M * ((L |^ n) / (n !)) by A19, A18, A15, XREAL_1:66;
hence abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) by XCMPLX_1:74; :: thesis: verum

end;

hence 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 !) ; :: thesis: verum

end;

hence ( 0 <= M & 0 <= L & ( 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, SIN_COS:54; :: thesis: verum