let n be Element of NAT ; :: thesis: for r, x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !)
let r, x, s be Real; :: thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) )
assume that
A1: x in ].(- r),r.[ and
A2: 0 < s and
A3: s < 1 ; :: thesis: abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !)
A4: abs ((s * x) - 0) = (abs s) * (abs x) by COMPLEX1:65
.= s * (abs x) by A2, ABSVALUE:def 1 ;
x in ].(0 - r),(0 + r).[ by A1;
then A5: abs (x - 0) < r by RCOMP_1:1;
abs x >= 0 by COMPLEX1:46;
then (abs x) * s < r * 1 by A2, A3, A5, XREAL_1:97;
then s * x in ].(0 - r),(0 + r).[ by A4, RCOMP_1:1;
then A6: s * x in dom (exp_R | ].(- r),r.[) by Th5;
(n + 1) ! > 0 by NEWTON:17;
then A7: abs ((n + 1) !) = (n + 1) ! by ABSVALUE:def 1;
abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) = abs ((((exp_R | ].(- r),r.[) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) by Th6
.= abs (((exp_R . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) by A6, FUNCT_1:47
.= (abs ((exp_R . (s * x)) * (x |^ (n + 1)))) / (abs ((n + 1) !)) by COMPLEX1:67
.= ((abs (exp_R . (s * x))) * (abs (x |^ (n + 1)))) / ((n + 1) !) by A7, COMPLEX1:65 ;
hence abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) by Th1; :: thesis: verum