let n be positive Nat; :: thesis: for c being real number st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
let c be real number ; :: thesis: ( c < 0 implies |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 )
n >= 0 + 1 by NAT_1:13;
then n + 1 >= 1 + 1 by XREAL_1:8;
then A1: (exp_R c) / (n + 1) <= (exp_R c) / 2 by XREAL_1:120;
assume c < 0 ; :: thesis: |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
then (exp_R c) / 2 < 1 / 2 by XREAL_1:76, SINCOS59ADD;
then A2: (exp_R c) / (n + 1) < 1 / 2 by A1, XXREAL_0:2;
A3: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2

proof

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

suppose A4: n is even ; :: thesis: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2

A5: (- 1) |^ n = (- 1) to_power n
.= 1 to_power n by POWER:54, A4
.= 1 by NEWTON:15 ;
- (1 / 2) < (exp_R c) / (n + 1) ;
hence |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by SEQ_2:9, A5, A2; :: thesis: verum

end;

suppose A6: not n is even ; :: thesis: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2

A7: (- 1) |^ n = (- 1) to_power n
.= - 1 by FIB_NUM2:3, A6 ;
- (1 / 2) < - ((exp_R c) / (n + 1)) by A2, XREAL_1:26;
hence |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A7, SEQ_2:9; :: thesis: verum

end;

end;

end;

((exp_R c) * ((- 1) |^ n)) / (n + 1) = ((exp_R c) * ((- 1) * (((- 1) |^ n) * (- 1)))) / (n + 1)
.= ((exp_R c) * ((- 1) * ((- 1) |^ (n + 1)))) / (n + 1) by NEWTON:11
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * (1 / (n + 1)))
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * (((n !) / (n !)) / (n + 1))) by XCMPLX_1:60
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * ((n !) / ((n !) * (n + 1)))) by XCMPLX_1:79
.= - ((((exp_R c) * ((- 1) |^ (n + 1))) * (n !)) / ((n + 1) * (n !)))
.= - ((((n !) * (exp_R c)) * ((- 1) |^ (n + 1))) / ((n + 1) !)) by NEWTON:21 ;
hence |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 by A3; :: thesis: verum