let r be Real; :: thesis: ( r > 0 implies ex r1, r2 being Real st
( r1 >= 0 & r2 >= 0 & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) ) ) )
assume A1: r > 0 ; :: thesis: ex r1, r2 being Real st
( r1 >= 0 & r2 >= 0 & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) ) )
take r1 = 1; :: thesis: ex r2 being Real st
( r1 >= 0 & r2 >= 0 & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) ) )
take r2 = r; :: thesis: ( r1 >= 0 & r2 >= 0 & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) ) )
thus ( r1 >= 0 & r2 >= 0 ) by A1; :: thesis: for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) )
let n be Nat; :: thesis: for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) )
let x, s be Real; :: thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies ( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) )
assume that
A2: x in ].(- r),r.[ and
A3: s > 0 and
A4: s < 1 ; :: thesis: ( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) )
x in ].(0 - r),(0 + r).[ by A2;
then A5: |.(x - 0).| < r by RCOMP_1:1;
A6: (|.x.| |^ n) / (n !) <= (r2 |^ n) / (n !)
proof
defpred S1[ Nat] means (|.x.| |^ $1) / ($1 !) <= (r2 |^ $1) / ($1 !);
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
A9: (|.x.| |^ (k + 1)) / ((k + 1) !) = ((|.x.| |^ k) * |.x.|) / ((k + 1) !) by NEWTON:6
.= ((|.x.| |^ k) * |.x.|) / ((k !) * (k + 1)) by NEWTON:15
.= (|.x.| |^ k) * (|.x.| / ((k !) * (k + 1))) by XCMPLX_1:74
.= (|.x.| |^ k) * ((|.x.| / (k !)) / (k + 1)) by XCMPLX_1:78
.= (|.x.| |^ k) * ((1 / ((k !) / |.x.|)) / (k + 1)) by XCMPLX_1:57
.= (|.x.| |^ k) * (((1 / (k !)) * |.x.|) / (k + 1)) by XCMPLX_1:82
.= ((|.x.| |^ k) * ((1 / (k !)) * |.x.|)) / (k + 1) by XCMPLX_1:74
.= (((|.x.| |^ k) * (1 / (k !))) * |.x.|) / (k + 1)
.= ((((|.x.| |^ k) * 1) / (k !)) * |.x.|) / (k + 1) by XCMPLX_1:74
.= (((|.x.| |^ k) / (k !)) * |.x.|) / (k + 1) ;
(|.x.| |^ k) / (k !) = |.(x |^ k).| / (k !) by Th1
.= |.(x |^ k).| / |.(k !).| by ABSVALUE:def 1
.= |.((x |^ k) / (k !)).| by COMPLEX1:67 ;
then A10: (|.x.| |^ k) / (k !) >= 0 by COMPLEX1:46;
A11: (r2 |^ (k + 1)) / ((k + 1) !) = ((r2 |^ k) * r2) / ((k + 1) !) by NEWTON:6
.= ((r2 |^ k) * r2) / ((k !) * (k + 1)) by NEWTON:15
.= (r2 |^ k) * (r2 / ((k !) * (k + 1))) by XCMPLX_1:74
.= (r2 |^ k) * ((r2 / (k !)) / (k + 1)) by XCMPLX_1:78
.= (r2 |^ k) * ((1 / ((k !) / r2)) / (k + 1)) by XCMPLX_1:57
.= (r2 |^ k) * (((1 / (k !)) * r2) / (k + 1)) by XCMPLX_1:82
.= ((r2 |^ k) * ((1 / (k !)) * r2)) / (k + 1) by XCMPLX_1:74
.= (((r2 |^ k) * (1 / (k !))) * r2) / (k + 1)
.= ((((r2 |^ k) * 1) / (k !)) * r2) / (k + 1) by XCMPLX_1:74
.= (((r2 |^ k) / (k !)) * r2) / (k + 1) ;
|.x.| >= 0 by COMPLEX1:46;
then ((|.x.| |^ k) / (k !)) * |.x.| <= ((r2 |^ k) / (k !)) * r2 by A5, A8, A10, XREAL_1:66;
hence S1[k + 1] by A9, A11, XREAL_1:72; :: thesis: verum
end;
(|.x.| |^ 0) / (0 !) = 1 / (0 !) by NEWTON:4
.= (r2 |^ 0) / (0 !) by NEWTON:4 ;
then A12: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A12, A7);
 hence (|.x.| |^ n) / (n !) <= (r2 |^ n) / (n !) ; :: thesis: verum
end;
|.x.| >= 0 by COMPLEX1:46;
then s * |.x.| < 1 * r by A3, A4, A5, XREAL_1:97;
then |.s.| * |.x.| < r by A3, ABSVALUE:def 1;
then |.((s * x) - 0).| < r by COMPLEX1:65;
then A13: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:1;
A14: for k being Nat holds |.((- 1) |^ k).| = 1
proof
let k be Nat; :: thesis: |.((- 1) |^ k).| = 1
per cases ( k is even or k is odd ) ;
suppose k is even ; :: thesis: |.((- 1) |^ k).| = 1
then consider j being Nat such that
A15: k = 2 * j by ABIAN:def 2;
thus |.((- 1) |^ k).| = |.(((- 1) |^ (1 + 1)) |^ j).| by A15, NEWTON:9
.= |.((((- 1) |^ 1) * (- 1)) |^ j).| by NEWTON:6
.= |.(((- 1) * (- 1)) |^ j).|
.= |.1.|
.= 1 by ABSVALUE:def 1 ; :: thesis: verum
end;
suppose k is odd ; :: thesis: |.((- 1) |^ k).| = 1
then consider j being Nat such that
A16: k = (2 * j) + 1 by ABIAN:9;
thus |.((- 1) |^ k).| = |.(((- 1) |^ (2 * j)) * (- 1)).| by A16, NEWTON:6
.= |.((((- 1) |^ (1 + 1)) |^ j) * (- 1)).| by NEWTON:9
.= |.(((((- 1) |^ 1) * (- 1)) |^ j) * (- 1)).| by NEWTON:6
.= |.((((- 1) * (- 1)) |^ j) * (- 1)).|
.= |.(1 * (- 1)).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ; :: thesis: verum
end;
end;
end;
A17: |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1
proof
per cases ( n is even or n is odd ) ;
suppose n is even ; :: thesis: |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1
then consider k being Nat such that
A18: n = 2 * k by ABIAN:def 2;
A19: dom (((- 1) |^ k) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A20: s * x in dom (sin | ].(- r),r.[) by A13, Th17;
A21: |.(sin (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ k) (#) (sin | ].(- r),r.[)) . (s * x)).| by A18, Th19
.= |.(((- 1) |^ k) * ((sin | ].(- r),r.[) . (s * x))).| by A13, A19, VALUED_1:def 5
.= |.((- 1) |^ k).| * |.((sin | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((sin | ].(- r),r.[) . (s * x)).| by A14
.= |.(sin . (s * x)).| by A20, FUNCT_1:47 ;
hence |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1 by A21, SIN_COS:def 17; :: thesis: verum
end;
suppose n is odd ; :: thesis: |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1
then consider k being Nat such that
A22: n = (2 * k) + 1 by ABIAN:9;
A23: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A24: s * x in dom (cos | ].(- r),r.[) by A13, Th17;
A25: |.(cos (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)).| by A22, Th19
.= |.(((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))).| by A13, A23, VALUED_1:def 5
.= |.((- 1) |^ k).| * |.((cos | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((cos | ].(- r),r.[) . (s * x)).| by A14
.= |.(cos . (s * x)).| by A24, FUNCT_1:47 ;
hence |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1 by A25, SIN_COS:def 19; :: thesis: verum
end;
end;
end;
A26: |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1
proof
per cases ( n is even or n is odd ) ;
suppose n is even ; :: thesis: |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1
then consider k being Nat such that
A27: n = 2 * k by ABIAN:def 2;
A28: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A29: s * x in dom (cos | ].(- r),r.[) by A13, Th17;
A30: |.(cos (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)).| by A27, Th19
.= |.(((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))).| by A13, A28, VALUED_1:def 5
.= |.((- 1) |^ k).| * |.((cos | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((cos | ].(- r),r.[) . (s * x)).| by A14
.= |.(cos . (s * x)).| by A29, FUNCT_1:47 ;
hence |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1 by A30, SIN_COS:def 19; :: thesis: verum
end;
suppose n is odd ; :: thesis: |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1
then consider k being Nat such that
A31: n = (2 * k) + 1 by ABIAN:9;
A32: dom (((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A33: s * x in dom (sin | ].(- r),r.[) by A13, Th17;
A34: |.(sin (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) . (s * x)).| by A31, Th19
.= |.(((- 1) |^ (k + 1)) * ((sin | ].(- r),r.[) . (s * x))).| by A13, A32, VALUED_1:def 5
.= |.((- 1) |^ (k + 1)).| * |.((sin | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((sin | ].(- r),r.[) . (s * x)).| by A14
.= |.(sin . (s * x)).| by A33, FUNCT_1:47 ;
hence |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1 by A34, SIN_COS:def 17; :: thesis: verum
end;
end;
end;
A35: |.((x |^ n) / (n !)).| = |.(x |^ n).| / |.(n !).| by COMPLEX1:67
.= |.(x |^ n).| / (n !) by ABSVALUE:def 1
.= (|.x.| |^ n) / (n !) by Th1 ;
then A36: (|.x.| |^ n) / (n !) >= 0 by COMPLEX1:46;
A37: |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| = |.((((diff (cos,].(- r),r.[)) . n) . (s * x)) * ((x |^ n) / (n !))).| by XCMPLX_1:74
.= |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| * |.((x |^ n) / (n !)).| by COMPLEX1:65
.= (|.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| * (|.x.| |^ n)) / (n !) by A35, XCMPLX_1:74 ;
A38: |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| = |.((((diff (sin,].(- r),r.[)) . n) . (s * x)) * ((x |^ n) / (n !))).| by XCMPLX_1:74
.= |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| * |.((x |^ n) / (n !)).| by COMPLEX1:65
.= (|.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| * (|.x.| |^ n)) / (n !) by A35, XCMPLX_1:74 ;
|.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| >= 0 by COMPLEX1:46;
then A39: |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| * ((|.x.| |^ n) / (n !)) <= r1 * ((r2 |^ n) / (n !)) by A36, A26, A6, XREAL_1:66;
|.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| >= 0 by COMPLEX1:46;
then |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| * ((|.x.| |^ n) / (n !)) <= r1 * ((r2 |^ n) / (n !)) by A36, A17, A6, XREAL_1:66;
hence ( |.(((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) & |.(((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (r1 * (r2 |^ n)) / (n !) ) by A38, A37, A39, XCMPLX_1:74; :: thesis: verum