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 ;
hence S1[k + 1] by ; :: thesis: verum
end;
() / () = 1 / () by NEWTON:4
.= (r2 |^ 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 ;
then |.s.| * |.x.| < r by ;
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
.= |.((((- 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
.= |.((((- 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 ;
A21: |.(sin (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ k) (#) (sin | ].(- r),r.[)) . (s * x)).| by
.= |.(((- 1) |^ k) * ((sin | ].(- r),r.[) . (s * x))).| by
.= |.((- 1) |^ k).| * |.((sin | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((sin | ].(- r),r.[) . (s * x)).| by A14
.= |.(sin . (s * x)).| by ;
hence |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1 by ; :: 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 ;
A25: |.(cos (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)).| by
.= |.(((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))).| by
.= |.((- 1) |^ k).| * |.((cos | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((cos | ].(- r),r.[) . (s * x)).| by A14
.= |.(cos . (s * x)).| by ;
hence |.(((diff (sin,].(- r),r.[)) . n) . (s * x)).| <= r1 by ; :: 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 ;
A30: |.(cos (s * x)).| <= 1 by SIN_COS:27;
|.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| = |.((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)).| by
.= |.(((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))).| by
.= |.((- 1) |^ k).| * |.((cos | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((cos | ].(- r),r.[) . (s * x)).| by A14
.= |.(cos . (s * x)).| by ;
hence |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1 by ; :: 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 ;
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
.= |.(((- 1) |^ (k + 1)) * ((sin | ].(- r),r.[) . (s * x))).| by
.= |.((- 1) |^ (k + 1)).| * |.((sin | ].(- r),r.[) . (s * x)).| by COMPLEX1:65
.= 1 * |.((sin | ].(- r),r.[) . (s * x)).| by A14
.= |.(sin . (s * x)).| by ;
hence |.(((diff (cos,].(- r),r.[)) . n) . (s * x)).| <= r1 by ; :: 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 ;
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 ;
|.(((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 ;
|.(((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 ;
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 ; :: thesis: verum