let n be positive Nat; :: thesis: for c being Real st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
let c be Real; :: 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:6;
then A1: (exp_R c) / (n + 1) <= (exp_R c) / 2 by XREAL_1:118;
assume c < 0 ; :: thesis: |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
then (exp_R c) / 2 < 1 / 2 by Th2, XREAL_1:74;
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 n is odd ) ;

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 A4, POWER:47
.= 1 ;
- (1 / 2) < (exp_R c) / (n + 1) ;
hence |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A5, A2, SEQ_2:1; :: thesis: verum

end;

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

A7: (- 1) |^ n = (- 1) to_power n
.= - 1 by A6, FIB_NUM2:2 ;
- (1 / 2) < - ((exp_R c) / (n + 1)) by A2, XREAL_1:24;
hence |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A7, SEQ_2:1; :: 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:6
.= - (((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:78
.= - ((((exp_R c) * ((- 1) |^ (n + 1))) * (n !)) / ((n + 1) * (n !)))
.= - ((((n !) * (exp_R c)) * ((- 1) |^ (n + 1))) / ((n + 1) !)) by NEWTON:15 ;
hence |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 by A3; :: thesis: verum