let r be Real; :: thesis: ( 0 < r implies ex M, L being Real st
( 0 <= M & 0 <= L & ( 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 !) ) ) )
assume A1: r > 0 ; :: thesis: ex M, L being Real st
( 0 <= M & 0 <= L & ( 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 !) ) )
take M = exp_R . r; :: thesis: ex L being Real st
( 0 <= M & 0 <= L & ( 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 !) ) )
take L = r; :: thesis: ( 0 <= M & 0 <= L & ( 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 !) ) )
now :: thesis: 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 !)
let n be Nat; :: thesis: 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 !)
now :: thesis: 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 !)
A2: for a, b being Real st 0 <= a & a <= b holds
for n being Nat holds
( 0 <= a |^ n & a |^ n <= b |^ n )
proof
let a, b be Real; :: thesis: ( 0 <= a & a <= b implies for n being Nat holds
( 0 <= a |^ n & a |^ n <= b |^ n ) )
assume that
A3: 0 <= a and
A4: a <= b ; :: thesis: for n being Nat holds
( 0 <= a |^ n & a |^ n <= b |^ n )
defpred S1[ Nat] means ( 0 <= a |^ $1 & a |^ $1 <= b |^ $1 );
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[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: S1[ 0 ] by NEWTON:4;
for n being Nat holds S1[n] from NAT_1:sch 2(A7, A5);
 hence for n being 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 |.(((((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: |.(((((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: |.(x - 0).| < r by RCOMP_1:1;
|.x.| >= 0 by COMPLEX1:46;
then A12: |.x.| |^ n <= L |^ n by A11, A2;
|.x.| >= 0 by COMPLEX1:46;
then s * |.x.| < 1 * r by A9, A10, A11, XREAL_1:97;
then |.s.| * |.x.| < r by A9, ABSVALUE:def 1;
then |.((s * x) - 0).| < r by COMPLEX1:65;
then A13: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:1;
then A14: |.(((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| = |.(((exp_R . (s * x)) * (x |^ n)) / (n !)).| by Th7
.= |.((exp_R . (s * x)) * ((x |^ n) / (n !))).| by XCMPLX_1:74
.= |.(exp_R . (s * x)).| * |.((x |^ n) / (n !)).| by COMPLEX1:65 ;
exp_R . (s * x) >= 0 by SIN_COS:54;
then A15: ( r in ([#] REAL) /\ (dom exp_R) & |.(exp_R . (s * x)).| = exp_R . (s * x) ) by ABSVALUE:def 1, TAYLOR_1:16, XREAL_0:def 1;
for x0 being Real holds 0 <= diff (exp_R,x0) by TAYLOR_1:16;
then A16: exp_R | ([#] REAL) is non-decreasing by FDIFF_2:39, TAYLOR_1:16;
|.((x |^ n) / (n !)).| = |.(x |^ n).| / |.(n !).| by COMPLEX1:67
.= |.(x |^ n).| / (n !) by ABSVALUE:def 1
.= (|.x.| |^ n) / (n !) by Th1 ;
then A17: |.((x |^ n) / (n !)).| <= (L |^ n) / (n !) by A12, XREAL_1:72;
A18: ( |.(exp_R . (s * x)).| >= 0 & |.((x |^ n) / (n !)).| >= 0 ) by COMPLEX1:46;
s * x in { p where p is Real : ( - r < p & p < r ) } by A13, RCOMP_1:def 2;
then consider g being Real such that
A19: ( g = s * x & - r < g & g < r ) ;
reconsider g = g as Element of REAL by XREAL_0:def 1;
( g = s * x & - r < g & g < r ) by A19;
then |.(exp_R . (s * x)).| <= M by A16, A15, RFUNCT_2:24, TAYLOR_1:16;
then |.(((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= M * ((L |^ n) / (n !)) by A18, A17, A14, XREAL_1:66;
hence |.(((((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
|.(((((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 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, SIN_COS:54; :: thesis: verum