let r be Real; :: thesis: ( r > 0 implies ex r1, r2 being Real st
( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((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 Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((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 Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((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 Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) )

now

let n be Element of NAT ; :: thesis: for x, s being Real st x in ].(- r),r.[ & s > 0 & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) )
let x, s be Real; :: thesis: ( x in ].(- r),r.[ & s > 0 & s < 1 implies ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((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: ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) )
x in ].(0 - r),(0 + r).[ by A2;
then A5: abs (x - 0) < r by RCOMP_1:1;
A6: ((abs x) |^ n) / (n !) <= (r2 |^ n) / (n !)

proof

defpred S₁[ Element of NAT ] means ((abs x) |^ $1) / ($1 !) <= (r2 |^ $1) / ($1 !);
A7: 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 A8: S₁[k] ; :: thesis: S₁[k + 1]
A9: ((abs x) |^ (k + 1)) / ((k + 1) !) = (((abs x) |^ k) * (abs x)) / ((k + 1) !) by NEWTON:6
.= (((abs x) |^ k) * (abs x)) / ((k !) * (k + 1)) by NEWTON:15
.= ((abs x) |^ k) * ((abs x) / ((k !) * (k + 1))) by XCMPLX_1:74
.= ((abs x) |^ k) * (((abs x) / (k !)) / (k + 1)) by XCMPLX_1:78
.= ((abs x) |^ k) * ((1 / ((k !) / (abs x))) / (k + 1)) by XCMPLX_1:57
.= ((abs x) |^ k) * (((1 / (k !)) * (abs x)) / (k + 1)) by XCMPLX_1:82
.= (((abs x) |^ k) * ((1 / (k !)) * (abs x))) / (k + 1) by XCMPLX_1:74
.= ((((abs x) |^ k) * (1 / (k !))) * (abs x)) / (k + 1)
.= (((((abs x) |^ k) * 1) / (k !)) * (abs x)) / (k + 1) by XCMPLX_1:74
.= ((((abs x) |^ k) / (k !)) * (abs x)) / (k + 1) ;
A10: k ! > 0 by NEWTON:17;
((abs x) |^ k) / (k !) = (abs (x |^ k)) / (k !) by Th1
.= (abs (x |^ k)) / (abs (k !)) by A10, ABSVALUE:def 1
.= abs ((x |^ k) / (k !)) by COMPLEX1:67 ;
then A11: ((abs x) |^ k) / (k !) >= 0 by COMPLEX1:46;
A12: (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) ;
abs x >= 0 by COMPLEX1:46;
then (((abs x) |^ k) / (k !)) * (abs x) <= ((r2 |^ k) / (k !)) * r2 by A5, A8, A11, XREAL_1:66;
hence S₁[k + 1] by A9, A12, XREAL_1:72; :: thesis: verum

end;

((abs x) |^ 0) / (0 !) = 1 / (0 !) by NEWTON:4
.= (r2 |^ 0) / (0 !) by NEWTON:4 ;
then A13: S₁[ 0 ] ;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A13, A7);
hence ((abs x) |^ n) / (n !) <= (r2 |^ n) / (n !) ; :: thesis: verum

end;

abs x >= 0 by COMPLEX1:46;
then s * (abs x) < 1 * r by A3, A4, A5, XREAL_1:97;
then (abs s) * (abs x) < r by A3, ABSVALUE:def 1;
then abs ((s * x) - 0) < r by COMPLEX1:65;
then A14: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:1;
A15: for k being Element of NAT holds abs ((- 1) |^ k) = 1

proof

let k be Element of NAT ; :: thesis: abs ((- 1) |^ k) = 1

per cases ( k is even or not k is even ) ;

suppose k is even ; :: thesis: abs ((- 1) |^ k) = 1

then consider j being Element of NAT such that
A16: k = 2 * j by ABIAN:def 2;
thus abs ((- 1) |^ k) = abs (((- 1) |^ (1 + 1)) |^ j) by A16, NEWTON:9
.= abs ((((- 1) |^ 1) * (- 1)) |^ j) by NEWTON:6
.= abs (((- 1) * (- 1)) |^ j) by NEWTON:5
.= abs 1 by NEWTON:10
.= 1 by ABSVALUE:def 1 ; :: thesis: verum

end;

suppose not k is even ; :: thesis: abs ((- 1) |^ k) = 1

then consider j being Element of NAT such that
A17: k = (2 * j) + 1 by ABIAN:9;
thus abs ((- 1) |^ k) = abs (((- 1) |^ (2 * j)) * (- 1)) by A17, NEWTON:6
.= abs ((((- 1) |^ (1 + 1)) |^ j) * (- 1)) by NEWTON:9
.= abs (((((- 1) |^ 1) * (- 1)) |^ j) * (- 1)) by NEWTON:6
.= abs ((((- 1) * (- 1)) |^ j) * (- 1)) by NEWTON:5
.= abs (1 * (- 1)) by NEWTON:10
.= abs 1 by COMPLEX1:52
.= 1 by ABSVALUE:def 1 ; :: thesis: verum

end;

end;

end;

A18: abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1

proof

per cases ( n is even or not n is even ) ;

suppose n is even ; :: thesis: abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1

then consider k being Element of NAT such that
A19: n = 2 * k by ABIAN:def 2;
A20: dom (((- 1) |^ k) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A21: s * x in dom (sin | ].(- r),r.[) by A14, Th17;
A22: abs (sin (s * x)) <= 1 by SIN_COS:27;
abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (sin | ].(- r),r.[)) . (s * x)) by A19, Th19
.= abs (((- 1) |^ k) * ((sin | ].(- r),r.[) . (s * x))) by A14, A20, VALUED_1:def 5
.= (abs ((- 1) |^ k)) * (abs ((sin | ].(- r),r.[) . (s * x))) by COMPLEX1:65
.= 1 * (abs ((sin | ].(- r),r.[) . (s * x))) by A15
.= abs (sin . (s * x)) by A21, FUNCT_1:47 ;
hence abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 by A22, SIN_COS:def 17; :: thesis: verum

end;

suppose not n is even ; :: thesis: abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1

then consider k being Element of NAT such that
A23: n = (2 * k) + 1 by ABIAN:9;
A24: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A25: s * x in dom (cos | ].(- r),r.[) by A14, Th17;
A26: abs (cos (s * x)) <= 1 by SIN_COS:27;
abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)) by A23, Th19
.= abs (((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))) by A14, A24, VALUED_1:def 5
.= (abs ((- 1) |^ k)) * (abs ((cos | ].(- r),r.[) . (s * x))) by COMPLEX1:65
.= 1 * (abs ((cos | ].(- r),r.[) . (s * x))) by A15
.= abs (cos . (s * x)) by A25, FUNCT_1:47 ;
hence abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 by A26, SIN_COS:def 19; :: thesis: verum

end;

end;

end;

A27: abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1

proof

per cases ( n is even or not n is even ) ;

suppose n is even ; :: thesis: abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1

then consider k being Element of NAT such that
A28: n = 2 * k by ABIAN:def 2;
A29: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A30: s * x in dom (cos | ].(- r),r.[) by A14, Th17;
A31: abs (cos (s * x)) <= 1 by SIN_COS:27;
abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)) by A28, Th19
.= abs (((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))) by A14, A29, VALUED_1:def 5
.= (abs ((- 1) |^ k)) * (abs ((cos | ].(- r),r.[) . (s * x))) by COMPLEX1:65
.= 1 * (abs ((cos | ].(- r),r.[) . (s * x))) by A15
.= abs (cos . (s * x)) by A30, FUNCT_1:47 ;
hence abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 by A31, SIN_COS:def 19; :: thesis: verum

end;

suppose not n is even ; :: thesis: abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1

then consider k being Element of NAT such that
A32: n = (2 * k) + 1 by ABIAN:9;
A33: dom (((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A34: s * x in dom (sin | ].(- r),r.[) by A14, Th17;
A35: abs (sin (s * x)) <= 1 by SIN_COS:27;
abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) . (s * x)) by A32, Th19
.= abs (((- 1) |^ (k + 1)) * ((sin | ].(- r),r.[) . (s * x))) by A14, A33, VALUED_1:def 5
.= (abs ((- 1) |^ (k + 1))) * (abs ((sin | ].(- r),r.[) . (s * x))) by COMPLEX1:65
.= 1 * (abs ((sin | ].(- r),r.[) . (s * x))) by A15
.= abs (sin . (s * x)) by A34, FUNCT_1:47 ;
hence abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 by A35, SIN_COS:def 17; :: thesis: verum

end;

end;

end;

A36: n ! > 0 by NEWTON:17;
A37: abs ((x |^ n) / (n !)) = (abs (x |^ n)) / (abs (n !)) by COMPLEX1:67
.= (abs (x |^ n)) / (n !) by A36, ABSVALUE:def 1
.= ((abs x) |^ n) / (n !) by Th1 ;
then A38: ((abs x) |^ n) / (n !) >= 0 by COMPLEX1:46;
A39: abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) = abs ((((diff (cos,].(- r),r.[)) . n) . (s * x)) * ((x |^ n) / (n !))) by XCMPLX_1:74
.= (abs (((diff (cos,].(- r),r.[)) . n) . (s * x))) * (abs ((x |^ n) / (n !))) by COMPLEX1:65
.= ((abs (((diff (cos,].(- r),r.[)) . n) . (s * x))) * ((abs x) |^ n)) / (n !) by A37, XCMPLX_1:74 ;
A40: abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) = abs ((((diff (sin,].(- r),r.[)) . n) . (s * x)) * ((x |^ n) / (n !))) by XCMPLX_1:74
.= (abs (((diff (sin,].(- r),r.[)) . n) . (s * x))) * (abs ((x |^ n) / (n !))) by COMPLEX1:65
.= ((abs (((diff (sin,].(- r),r.[)) . n) . (s * x))) * ((abs x) |^ n)) / (n !) by A37, XCMPLX_1:74 ;
abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) >= 0 by COMPLEX1:46;
then A41: (abs (((diff (cos,].(- r),r.[)) . n) . (s * x))) * (((abs x) |^ n) / (n !)) <= r1 * ((r2 |^ n) / (n !)) by A38, A27, A6, XREAL_1:66;
abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) >= 0 by COMPLEX1:46;
then (abs (((diff (sin,].(- r),r.[)) . n) . (s * x))) * (((abs x) |^ n) / (n !)) <= r1 * ((r2 |^ n) / (n !)) by A38, A18, A6, XREAL_1:66;
hence ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) by A40, A39, A41, XCMPLX_1:74; :: thesis: verum

end;

hence ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) by A1; :: thesis: verum