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 A2: ( x in ].(- r),r.[ & s > 0 & 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 A3: abs (x - 0 ) < r by RCOMP_1:8;
abs x >= 0 by COMPLEX1:132;
then s * (abs x) < 1 * r by A2, A3, XREAL_1:99;
then (abs s) * (abs x) < r by A2, ABSVALUE:def 1;
then abs ((s * x) - 0 ) < r by COMPLEX1:151;
then A4: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:8;
A5: n ! > 0 by NEWTON:23;
A6: abs ((x |^ n) / (n ! )) = (abs (x |^ n)) / (abs (n ! )) by COMPLEX1:153
.= (abs (x |^ n)) / (n ! ) by A5, ABSVALUE:def 1
.= ((abs x) |^ n) / (n ! ) by Th1 ;
A7: 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:75
.= (abs (((diff sin ,].(- r),r.[) . n) . (s * x))) * (abs ((x |^ n) / (n ! ))) by COMPLEX1:151
.= ((abs (((diff sin ,].(- r),r.[) . n) . (s * x))) * ((abs x) |^ n)) / (n ! ) by A6, XCMPLX_1:75 ;
A8: 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:75
.= (abs (((diff cos ,].(- r),r.[) . n) . (s * x))) * (abs ((x |^ n) / (n ! ))) by COMPLEX1:151
.= ((abs (((diff cos ,].(- r),r.[) . n) . (s * x))) * ((abs x) |^ n)) / (n ! ) by A6, XCMPLX_1:75 ;
A9: abs (((diff sin ,].(- r),r.[) . n) . (s * x)) >= 0 by COMPLEX1:132;
A10: abs (((diff cos ,].(- r),r.[) . n) . (s * x)) >= 0 by COMPLEX1:132;
A11: ((abs x) |^ n) / (n ! ) >= 0 by A6, COMPLEX1:132;
A12: 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
A13: k = 2 * j by ABIAN:def 2;
thus abs ((- 1) |^ k) = abs (((- 1) |^ (1 + 1)) |^ j) by A13, NEWTON:14
.= abs ((((- 1) |^ 1) * (- 1)) |^ j) by NEWTON:11
.= abs (((- 1) * (- 1)) |^ j) by NEWTON:10
.= abs 1 by NEWTON:15
.= 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
A14: k = (2 * j) + 1 by ABIAN:9;
thus abs ((- 1) |^ k) = abs (((- 1) |^ (2 * j)) * (- 1)) by A14, NEWTON:11
.= abs ((((- 1) |^ (1 + 1)) |^ j) * (- 1)) by NEWTON:14
.= abs (((((- 1) |^ 1) * (- 1)) |^ j) * (- 1)) by NEWTON:11
.= abs ((((- 1) * (- 1)) |^ j) * (- 1)) by NEWTON:10
.= abs (1 * (- 1)) by NEWTON:15
.= abs 1 by COMPLEX1:138
.= 1 by ABSVALUE:def 1 ; :: thesis: verum

end;

end;

end;

A15: 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
A16: n = 2 * k by ABIAN:def 2;
A17: dom (((- 1) |^ k) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A18: s * x in dom (sin | ].(- r),r.[) by A4, Th17;
A19: abs (((diff sin ,].(- r),r.[) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (sin | ].(- r),r.[)) . (s * x)) by A16, Th19
.= abs (((- 1) |^ k) * ((sin | ].(- r),r.[) . (s * x))) by A4, A17, VALUED_1:def 5
.= (abs ((- 1) |^ k)) * (abs ((sin | ].(- r),r.[) . (s * x))) by COMPLEX1:151
.= 1 * (abs ((sin | ].(- r),r.[) . (s * x))) by A12
.= abs (sin . (s * x)) by A18, FUNCT_1:70 ;
abs (sin (s * x)) <= 1 by SIN_COS:30;
hence abs (((diff sin ,].(- r),r.[) . n) . (s * x)) <= r1 by A19, SIN_COS:def 21; :: 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
A20: n = (2 * k) + 1 by ABIAN:9;
A21: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A22: s * x in dom (cos | ].(- r),r.[) by A4, Th17;
A23: abs (((diff sin ,].(- r),r.[) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)) by A20, Th19
.= abs (((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))) by A4, A21, VALUED_1:def 5
.= (abs ((- 1) |^ k)) * (abs ((cos | ].(- r),r.[) . (s * x))) by COMPLEX1:151
.= 1 * (abs ((cos | ].(- r),r.[) . (s * x))) by A12
.= abs (cos . (s * x)) by A22, FUNCT_1:70 ;
abs (cos (s * x)) <= 1 by SIN_COS:30;
hence abs (((diff sin ,].(- r),r.[) . n) . (s * x)) <= r1 by A23, SIN_COS:def 23; :: thesis: verum

end;

end;

end;

A24: 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
A25: n = 2 * k by ABIAN:def 2;
A26: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A27: s * x in dom (cos | ].(- r),r.[) by A4, Th17;
A28: abs (((diff cos ,].(- r),r.[) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)) by A25, Th19
.= abs (((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))) by A4, A26, VALUED_1:def 5
.= (abs ((- 1) |^ k)) * (abs ((cos | ].(- r),r.[) . (s * x))) by COMPLEX1:151
.= 1 * (abs ((cos | ].(- r),r.[) . (s * x))) by A12
.= abs (cos . (s * x)) by A27, FUNCT_1:70 ;
abs (cos (s * x)) <= 1 by SIN_COS:30;
hence abs (((diff cos ,].(- r),r.[) . n) . (s * x)) <= r1 by A28, SIN_COS:def 23; :: 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
A29: n = (2 * k) + 1 by ABIAN:9;
A30: dom (((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def 5
.= ].(- r),r.[ by Th17 ;
A31: s * x in dom (sin | ].(- r),r.[) by A4, Th17;
A32: abs (((diff cos ,].(- r),r.[) . n) . (s * x)) = abs ((((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) . (s * x)) by A29, Th19
.= abs (((- 1) |^ (k + 1)) * ((sin | ].(- r),r.[) . (s * x))) by A4, A30, VALUED_1:def 5
.= (abs ((- 1) |^ (k + 1))) * (abs ((sin | ].(- r),r.[) . (s * x))) by COMPLEX1:151
.= 1 * (abs ((sin | ].(- r),r.[) . (s * x))) by A12
.= abs (sin . (s * x)) by A31, FUNCT_1:70 ;
abs (sin (s * x)) <= 1 by SIN_COS:30;
hence abs (((diff cos ,].(- r),r.[) . n) . (s * x)) <= r1 by A32, SIN_COS:def 21; :: thesis: verum

end;

end;

end;

((abs x) |^ n) / (n ! ) <= (r2 |^ n) / (n ! )

proof

defpred S₁[ Element of NAT ] means ((abs x) |^ $1) / ($1 ! ) <= (r2 |^ $1) / ($1 ! );
A33: S₁[ 0 ]

proof

((abs x) |^ 0 ) / (0 ! ) = 1 / (0 ! ) by NEWTON:9
.= (r2 |^ 0 ) / (0 ! ) by NEWTON:9 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A34: 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 A35: S₁[k] ; :: thesis: S₁[k + 1]
A36: ((abs x) |^ (k + 1)) / ((k + 1) ! ) = (((abs x) |^ k) * (abs x)) / ((k + 1) ! ) by NEWTON:11
.= (((abs x) |^ k) * (abs x)) / ((k ! ) * (k + 1)) by NEWTON:21
.= ((abs x) |^ k) * ((abs x) / ((k ! ) * (k + 1))) by XCMPLX_1:75
.= ((abs x) |^ k) * (((abs x) / (k ! )) / (k + 1)) by XCMPLX_1:79
.= ((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:83
.= (((abs x) |^ k) * ((1 / (k ! )) * (abs x))) / (k + 1) by XCMPLX_1:75
.= ((((abs x) |^ k) * (1 / (k ! ))) * (abs x)) / (k + 1)
.= (((((abs x) |^ k) * 1) / (k ! )) * (abs x)) / (k + 1) by XCMPLX_1:75
.= ((((abs x) |^ k) / (k ! )) * (abs x)) / (k + 1) ;
A37: (r2 |^ (k + 1)) / ((k + 1) ! ) = ((r2 |^ k) * r2) / ((k + 1) ! ) by NEWTON:11
.= ((r2 |^ k) * r2) / ((k ! ) * (k + 1)) by NEWTON:21
.= (r2 |^ k) * (r2 / ((k ! ) * (k + 1))) by XCMPLX_1:75
.= (r2 |^ k) * ((r2 / (k ! )) / (k + 1)) by XCMPLX_1:79
.= (r2 |^ k) * ((1 / ((k ! ) / r2)) / (k + 1)) by XCMPLX_1:57
.= (r2 |^ k) * (((1 / (k ! )) * r2) / (k + 1)) by XCMPLX_1:83
.= ((r2 |^ k) * ((1 / (k ! )) * r2)) / (k + 1) by XCMPLX_1:75
.= (((r2 |^ k) * (1 / (k ! ))) * r2) / (k + 1)
.= ((((r2 |^ k) * 1) / (k ! )) * r2) / (k + 1) by XCMPLX_1:75
.= (((r2 |^ k) / (k ! )) * r2) / (k + 1) ;
A38: k ! > 0 by NEWTON:23;
((abs x) |^ k) / (k ! ) = (abs (x |^ k)) / (k ! ) by Th1
.= (abs (x |^ k)) / (abs (k ! )) by A38, ABSVALUE:def 1
.= abs ((x |^ k) / (k ! )) by COMPLEX1:153 ;
then A39: ((abs x) |^ k) / (k ! ) >= 0 by COMPLEX1:132;
abs x >= 0 by COMPLEX1:132;
then (((abs x) |^ k) / (k ! )) * (abs x) <= ((r2 |^ k) / (k ! )) * r2 by A3, A35, A39, XREAL_1:68;
hence S₁[k + 1] by A36, A37, XREAL_1:74; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A33, A34);
hence ((abs x) |^ n) / (n ! ) <= (r2 |^ n) / (n ! ) ; :: thesis: verum

end;

then ( (abs (((diff sin ,].(- r),r.[) . n) . (s * x))) * (((abs x) |^ n) / (n ! )) <= r1 * ((r2 |^ n) / (n ! )) & (abs (((diff cos ,].(- r),r.[) . n) . (s * x))) * (((abs x) |^ n) / (n ! )) <= r1 * ((r2 |^ n) / (n ! )) ) by A9, A10, A11, A15, A24, XREAL_1:68;
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 A7, A8, XCMPLX_1:75; :: 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