let x be Element of REAL ; :: thesis: 1 + x <= exp_R . x

per cases ( x > 0 or x = 0 or x < 0 ) ;

suppose A1: x > 0 ; :: thesis: 1 + x <= exp_R . x

reconsider 1x = 1 + x as Element of REAL by XREAL_0:def 1;
set B2 = NAT --> 1x;
A2: for n being Nat st x > 0 holds
(NAT --> 1x) . n <= (Partial_Sums (x rExpSeq)) . (n + 1)

proof

let n be Nat; :: thesis: ( x > 0 implies (NAT --> 1x) . n <= (Partial_Sums (x rExpSeq)) . (n + 1) )
defpred S₁[ Nat] means (NAT --> 1x) . $1 <= (Partial_Sums (x rExpSeq)) . (1 + $1);
(Partial_Sums (x rExpSeq)) . 1 = ((Partial_Sums (x rExpSeq)) . 0) + ((x rExpSeq) . (0 + 1)) by SERIES_1:def 1;
then A3: (Partial_Sums (x rExpSeq)) . 1 = ((x rExpSeq) . 0) + ((x rExpSeq) . 1) by SERIES_1:def 1;
A4: (x rExpSeq) . 0 = (x |^ 0) / (0 !) by SIN_COS:def 5
.= 1 by NEWTON:4, NEWTON:12 ;
(x rExpSeq) . 1 = (x |^ 1) / (1 !) by SIN_COS:def 5;
then A5: S₁[ 0 ] by A4, A3, NEWTON:13;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: (Partial_Sums (x rExpSeq)) . (1 + (k + 1)) = ((Partial_Sums (x rExpSeq)) . (k + 1)) + ((x rExpSeq) . ((k + 1) + 1)) by SERIES_1:def 1;
A9: (x rExpSeq) . ((k + 1) + 1) > 0

proof

( x |^ ((k + 1) + 1) > 0 & ((k + 1) + 1) ! > 0 ) by A1, NEWTON:83;
then (x |^ ((k + 1) + 1)) / (((k + 1) + 1) !) > 0 ;
hence (x rExpSeq) . ((k + 1) + 1) > 0 by SIN_COS:def 5; :: thesis: verum

end;

A10: 1 + x <= (Partial_Sums (x rExpSeq)) . (k + 1) by A7, FUNCOP_1:7, ORDINAL1:def 12;
(Partial_Sums (x rExpSeq)) . (k + 1) <= ((x rExpSeq) . ((k + 1) + 1)) + ((Partial_Sums (x rExpSeq)) . (k + 1)) by A9, XREAL_1:31;
hence S₁[k + 1] by A8, A10, XXREAL_0:2; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence ( x > 0 implies (NAT --> 1x) . n <= (Partial_Sums (x rExpSeq)) . (n + 1) ) ; :: thesis: verum

end;

A11: for n being Nat holds (NAT --> 1x) . n <= ((Partial_Sums (x rExpSeq)) ^\ 1) . n

proof

let n be Nat; :: thesis: (NAT --> 1x) . n <= ((Partial_Sums (x rExpSeq)) ^\ 1) . n
(NAT --> 1x) . n <= (Partial_Sums (x rExpSeq)) . (n + 1) by A1, A2;
hence (NAT --> 1x) . n <= ((Partial_Sums (x rExpSeq)) ^\ 1) . n by NAT_1:def 3; :: thesis: verum

end;

A12: lim (NAT --> 1x) = (NAT --> 1x) . 1 by SEQ_4:26
.= 1 + x ;
A13: Partial_Sums (x rExpSeq) is convergent by SERIES_1:def 2, SIN_COS:45;
then A14: ( lim ((Partial_Sums (x rExpSeq)) ^\ 1) = lim (Partial_Sums (x rExpSeq)) & (Partial_Sums (x rExpSeq)) ^\ 1 is convergent ) by SEQ_4:20;
lim (NAT --> 1x) <= lim ((Partial_Sums (x rExpSeq)) ^\ 1) by A13, A11, SEQ_2:18;
then lim (NAT --> 1x) <= Sum (x rExpSeq) by A14, SERIES_1:def 3;
hence 1 + x <= exp_R . x by A12, SIN_COS:def 22; :: thesis: verum

end;

suppose x = 0 ; :: thesis: 1 + x <= exp_R . x

hence 1 + x <= exp_R . x by SIN_COS:51; :: thesis: verum

end;

suppose A15: x < 0 ; :: thesis: 1 + x <= exp_R . x

set y = - x;
1 - (- x) <= exp_R . (- (- x))

proof

per cases ( - x <= 1 or - x > 1 ) ;

suppose A16: - x <= 1 ; :: thesis: 1 - (- x) <= exp_R . (- (- x))

for x being Element of REAL st x > 0 & x <= 1 holds
1 - x <= exp_R . (- x)

proof

let x be Element of REAL ; :: thesis: ( x > 0 & x <= 1 implies 1 - x <= exp_R . (- x) )
assume that
A17: x > 0 and
A18: x <= 1 ; :: thesis: 1 - x <= exp_R . (- x)
reconsider 1x = 1 - x as Element of REAL by XREAL_0:def 1;
set B2 = NAT --> 1x;
A19: for n being Nat holds (NAT --> 1x) . n <= (Partial_Sums ((- x) rExpSeq)) . (n + 1)

proof

let n be Nat; :: thesis: (NAT --> 1x) . n <= (Partial_Sums ((- x) rExpSeq)) . (n + 1)
defpred S₁[ Nat] means (NAT --> 1x) . $1 <= (Partial_Sums ((- x) rExpSeq)) . ($1 + 1);
(Partial_Sums ((- x) rExpSeq)) . (0 + 1) = ((Partial_Sums ((- x) rExpSeq)) . 0) + (((- x) rExpSeq) . 1) by SERIES_1:def 1;
then A20: (Partial_Sums ((- x) rExpSeq)) . (0 + 1) = (((- x) rExpSeq) . 0) + (((- x) rExpSeq) . 1) by SERIES_1:def 1;
((- x) rExpSeq) . 1 = ((- x) |^ 1) / (1 !) by SIN_COS:def 5;
then A21: ((- x) rExpSeq) . 1 = - x by NEWTON:13;
((- x) rExpSeq) . 0 = ((- x) |^ 0) / (0 !) by SIN_COS:def 5
.= 1 by NEWTON:4, NEWTON:12 ;
then A22: S₁[ 0 ] by A21, A20;
A23: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A24: S₁[k] ; :: thesis: S₁[k + 1]

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

suppose k is even ; :: thesis: S₁[k + 1]

then consider m being Nat such that
A25: k = 2 * m by ABIAN:def 2;
A26: 1 - x <= (Partial_Sums ((- x) rExpSeq)) . (k + 1) by A24, FUNCOP_1:7, ORDINAL1:def 12;
A27: for k being Element of NAT st k is even & k > 0 holds
for y being Real holds (y rExpSeq) . k >= 0

proof

let k be Element of NAT ; :: thesis: ( k is even & k > 0 implies for y being Real holds (y rExpSeq) . k >= 0 )
assume that
A28: k is even and
A29: k > 0 ; :: thesis: for y being Real holds (y rExpSeq) . k >= 0
let y be Real; :: thesis: (y rExpSeq) . k >= 0

per cases ( y > 0 or y = 0 or y < 0 ) ;

suppose y > 0 ; :: thesis: (y rExpSeq) . k >= 0

then y |^ k > 0 by NEWTON:83;
then (y |^ k) / (k !) > 0 ;
hence (y rExpSeq) . k >= 0 by SIN_COS:def 5; :: thesis: verum

end;

suppose y = 0 ; :: thesis: (y rExpSeq) . k >= 0

then y |^ k = 0 by A29, NEWTON:84;
then (y |^ k) / (k !) = 0 ;
hence (y rExpSeq) . k >= 0 by SIN_COS:def 5; :: thesis: verum

end;

suppose A31: y < 0 ; :: thesis: (y rExpSeq) . k >= 0

consider m being Nat such that
A32: k = 2 * m by A28, ABIAN:def 2;
y |^ k = y |^ (m + m) by A32;
then y |^ k = (y |^ m) * (y |^ m) by NEWTON:8;
then y |^ k = (y * y) |^ m by NEWTON:7;
then y |^ k >= 0 by A31, NEWTON:83;
then (y |^ k) / (k !) >= 0 ;
hence (y rExpSeq) . k >= 0 by SIN_COS:def 5; :: thesis: verum

end;

end;

end;

((- x) rExpSeq) . (k + 2) >= 0 by A25, A27;
then A35: (Partial_Sums ((- x) rExpSeq)) . (k + 1) <= ((Partial_Sums ((- x) rExpSeq)) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) by XREAL_1:31;
1 - x <= ((Partial_Sums ((- x) rExpSeq)) . (k + 1)) + (((- x) rExpSeq) . ((k + 1) + 1)) by A26, A35, XXREAL_0:2;
hence S₁[k + 1] by SERIES_1:def 1; :: thesis: verum

end;

suppose k is odd ; :: thesis: S₁[k + 1]

then consider m being Nat such that
A36: k = (2 * m) + 1 by ABIAN:9;
for k being Element of NAT
for x being Element of REAL st k is odd & x > 0 & x <= 1 holds
1 - x <= (Partial_Sums ((- x) rExpSeq)) . k

proof

let k be Element of NAT ; :: thesis: for x being Element of REAL st k is odd & x > 0 & x <= 1 holds
1 - x <= (Partial_Sums ((- x) rExpSeq)) . k
let x be Element of REAL ; :: thesis: ( k is odd & x > 0 & x <= 1 implies 1 - x <= (Partial_Sums ((- x) rExpSeq)) . k )
assume A38: k is odd ; :: thesis: ( not x > 0 or not x <= 1 or 1 - x <= (Partial_Sums ((- x) rExpSeq)) . k )
assume A39: x > 0 ; :: thesis: ( not x <= 1 or 1 - x <= (Partial_Sums ((- x) rExpSeq)) . k )
assume A40: x <= 1 ; :: thesis: 1 - x <= (Partial_Sums ((- x) rExpSeq)) . k
defpred S₂[ Nat] means 1 - x <= (Partial_Sums ((- x) rExpSeq)) . ((2 * $1) + 1);
(Partial_Sums ((- x) rExpSeq)) . ((2 * 0) + 1) = ((Partial_Sums ((- x) rExpSeq)) . 0) + (((- x) rExpSeq) . 1) by SERIES_1:def 1;
then A41: (Partial_Sums ((- x) rExpSeq)) . ((2 * 0) + 1) = (((- x) rExpSeq) . 0) + (((- x) rExpSeq) . 1) by SERIES_1:def 1;
A42: ((- x) rExpSeq) . 0 = ((- x) |^ 0) / (0 !) by SIN_COS:def 5
.= 1 by NEWTON:4, NEWTON:12 ;
((- x) rExpSeq) . 1 = ((- x) |^ 1) / (1 !) by SIN_COS:def 5;
then A44: S₂[ 0 ] by A41, A42, NEWTON:13;
A45: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A46: S₂[k] ; :: thesis: S₂[k + 1]
(Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 1) <= (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3)

proof

(Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3) = ((Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 2)) + (((- x) rExpSeq) . (((2 * k) + 2) + 1)) by SERIES_1:def 1;
then (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3) = ((Partial_Sums ((- x) rExpSeq)) . (((2 * k) + 1) + 1)) + (((- x) rExpSeq) . ((2 * k) + 3)) ;
then (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3) = (((Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 1)) + (((- x) rExpSeq) . ((2 * k) + 2))) + (((- x) rExpSeq) . ((2 * k) + 3)) by SERIES_1:def 1;
then A47: (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3) = ((Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 1)) + ((((- x) rExpSeq) . ((2 * k) + 2)) + (((- x) rExpSeq) . ((2 * k) + 3))) ;
(((- x) rExpSeq) . (((2 * k) + 1) + 1)) + (((- x) rExpSeq) . (((2 * k) + 1) + 2)) >= 0 by A39, A40, Th1;
hence (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 1) <= (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3) by A47, XREAL_1:31; :: thesis: verum

end;

hence S₂[k + 1] by A46, XXREAL_0:2; :: thesis: verum

end;

A48: for k being Nat holds S₂[k] from NAT_1:sch 2(A44, A45);
consider m being Nat such that
A49: k = (2 * m) + 1 by A38, ABIAN:9;
thus 1 - x <= (Partial_Sums ((- x) rExpSeq)) . k by A48, A49; :: thesis: verum

end;

hence S₁[k + 1] by A36, A17, A18; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A22, A23);
hence (NAT --> 1x) . n <= (Partial_Sums ((- x) rExpSeq)) . (n + 1) ; :: thesis: verum

end;

A50: for n being Nat holds (NAT --> 1x) . n <= ((Partial_Sums ((- x) rExpSeq)) ^\ 1) . n

proof

let n be Nat; :: thesis: (NAT --> 1x) . n <= ((Partial_Sums ((- x) rExpSeq)) ^\ 1) . n
(NAT --> 1x) . n <= (Partial_Sums ((- x) rExpSeq)) . (n + 1) by A19;
hence (NAT --> 1x) . n <= ((Partial_Sums ((- x) rExpSeq)) ^\ 1) . n by NAT_1:def 3; :: thesis: verum

end;

A51: lim (NAT --> 1x) = (NAT --> 1x) . 1 by SEQ_4:26
.= 1 - x ;
A52: Partial_Sums ((- x) rExpSeq) is convergent by SERIES_1:def 2, SIN_COS:45;
then A53: ( lim ((Partial_Sums ((- x) rExpSeq)) ^\ 1) = lim (Partial_Sums ((- x) rExpSeq)) & (Partial_Sums ((- x) rExpSeq)) ^\ 1 is convergent ) by SEQ_4:20;
lim (NAT --> 1x) <= lim ((Partial_Sums ((- x) rExpSeq)) ^\ 1) by A52, A50, SEQ_2:18;
then lim (NAT --> 1x) <= Sum ((- x) rExpSeq) by A53, SERIES_1:def 3;
hence 1 - x <= exp_R . (- x) by A51, SIN_COS:def 22; :: thesis: verum

end;

hence 1 - (- x) <= exp_R . (- (- x)) by A15, A16; :: thesis: verum

end;

suppose A54: - x > 1 ; :: thesis: 1 - (- x) <= exp_R . (- (- x))

then 0 < exp_R . (- (- x)) by SIN_COS:53;
hence 1 - (- x) <= exp_R . (- (- x)) by A54, XREAL_1:49; :: thesis: verum

end;

end;

end;

hence 1 + x <= exp_R . x ; :: thesis: verum

end;

end;