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

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 A2: ( x in ].(- r),r.[ & 0 < s & 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 A2;
then A3: abs (x - 0 ) < r by RCOMP_1:8;
abs x >= 0 by COMPLEX1:132;
then s * (abs x) < 1 * r by A2, A3, XREAL_1:99;
then (abs s) * (abs x) < r by A2, ABSVALUE:def 1;
then abs ((s * x) - 0 ) < r by COMPLEX1:151;
then A4: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:8;
A5: abs (exp_R . (s * x)) >= 0 by COMPLEX1:132;
A6: abs ((x |^ n) / (n ! )) >= 0 by COMPLEX1:132;
X: [#] REAL c= dom exp_R by SIN_COS:51;
( exp_R is_differentiable_on [#] REAL & ( for x0 being Real holds 0 <= diff exp_R ,x0 ) ) by TAYLOR_1:16;
then A7: exp_R | ([#] REAL ) is non-decreasing by X, FDIFF_2:39;
s * x in { p where p is Real : ( - r < p & p < r ) } by A4, RCOMP_1:def 2;
then A8: ex g being Real st
( g = s * x & - r < g & g < r ) ;
A9: r in ([#] REAL ) /\ (dom exp_R ) by TAYLOR_1:16;
exp_R . (s * x) >= 0 by SIN_COS:59;
then abs (exp_R . (s * x)) = exp_R . (s * x) by ABSVALUE:def 1;
then A10: abs (exp_R . (s * x)) <= M by A7, A8, A9, RFUNCT_2:48, TAYLOR_1:16;
A11: n ! > 0 by NEWTON:23;
A12: abs ((x |^ n) / (n ! )) = (abs (x |^ n)) / (abs (n ! )) by COMPLEX1:153
.= (abs (x |^ n)) / (n ! ) by A11, ABSVALUE:def 1
.= ((abs x) |^ n) / (n ! ) by Th1 ;
A13: 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 A14: ( 0 <= a & 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 );
A15: S₁[ 0 ]

proof

A16: b |^ 0 = 1 by NEWTON:9;
thus 0 <= a |^ 0 by NEWTON:9; :: thesis: a |^ 0 <= b |^ 0
thus a |^ 0 <= b |^ 0 by A16, NEWTON:9; :: thesis: verum

end;

A17: 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 A18: S₁[k] ; :: thesis: S₁[k + 1]
A19: b |^ (k + 1) = (b |^ k) * b by NEWTON:11;
0 * a <= (a |^ k) * a by A14, A18;
hence a |^ (k + 1) >= 0 by NEWTON:11; :: thesis: a |^ (k + 1) <= b |^ (k + 1)
(a |^ k) * a <= (b |^ k) * b by A14, A18, XREAL_1:68;
hence a |^ (k + 1) <= b |^ (k + 1) by A19, NEWTON:11; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A15, A17);
hence for n being Element of NAT holds
( 0 <= a |^ n & a |^ n <= b |^ n ) ; :: thesis: verum

end;

abs x >= 0 by COMPLEX1:132;
then (abs x) |^ n <= L |^ n by A3, A13;
then A20: abs ((x |^ n) / (n ! )) <= (L |^ n) / (n ! ) by A11, A12, XREAL_1:74;
abs (((((diff exp_R ,].(- r),r.[) . n) . (s * x)) * (x |^ n)) / (n ! )) = abs (((exp_R . (s * x)) * (x |^ n)) / (n ! )) by A4, Th7
.= abs ((exp_R . (s * x)) * ((x |^ n) / (n ! ))) by XCMPLX_1:75
.= (abs (exp_R . (s * x))) * (abs ((x |^ n) / (n ! ))) by COMPLEX1:151 ;
then abs (((((diff exp_R ,].(- r),r.[) . n) . (s * x)) * (x |^ n)) / (n ! )) <= M * ((L |^ n) / (n ! )) by A5, A6, A10, A20, XREAL_1:68;
hence abs (((((diff exp_R ,].(- r),r.[) . n) . (s * x)) * (x |^ n)) / (n ! )) <= (M * (L |^ n)) / (n ! ) by XCMPLX_1:75; :: 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:59; :: thesis: verum