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 <= () . (n + 1)
proof
let n be Nat; :: thesis: ( x > 0 implies (NAT --> 1x) . n <= () . (n + 1) )
defpred S1[ Nat] means (NAT --> 1x) . \$1 <= () . (1 + \$1);
(Partial_Sums ()) . 1 = (() . 0) + (() . (0 + 1)) by SERIES_1:def 1;
then A3: (Partial_Sums ()) . 1 = (() . 0) + (() . 1) by SERIES_1:def 1;
A4: () . 0 = (x |^ 0) / () by SIN_COS:def 5
.= 1 by ;
(x rExpSeq) . 1 = (x |^ 1) / (1 !) by SIN_COS:def 5;
then (x rExpSeq) . 1 = x by NEWTON:13;
then A5: S1[ 0 ] by A4, A3;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
A8: (Partial_Sums ()) . (1 + (k + 1)) = (() . (k + 1)) + (() . ((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 ;
then (x |^ ((k + 1) + 1)) / (((k + 1) + 1) !) > 0 ;
hence (x rExpSeq) . ((k + 1) + 1) > 0 by SIN_COS:def 5; :: thesis: verum
end;
k in NAT by ORDINAL1:def 12;
then A10: 1 + x <= () . (k + 1) by ;
(Partial_Sums ()) . (k + 1) <= (() . ((k + 1) + 1)) + (() . (k + 1)) by ;
then 1 + x <= (() . (k + 1)) + (() . ((k + 1) + 1)) by ;
hence S1[k + 1] by A8; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A5, A6);
hence ( x > 0 implies (NAT --> 1x) . n <= () . (n + 1) ) ; :: thesis: verum
end;
A11: for n being Nat holds (NAT --> 1x) . n <= (() ^\ 1) . n
proof
let n be Nat; :: thesis: (NAT --> 1x) . n <= (() ^\ 1) . n
(NAT --> 1x) . n <= () . (n + 1) by A1, A2;
hence (NAT --> 1x) . n <= (() ^\ 1) . n by NAT_1:def 3; :: thesis: verum
end;
A12: lim (NAT --> 1x) = (NAT --> 1x) . 1 by SEQ_4:26
.= 1 + x ;
x rExpSeq is summable by SIN_COS:45;
then A13: Partial_Sums () is convergent by SERIES_1:def 2;
then A14: ( lim (() ^\ 1) = lim () & () ^\ 1 is convergent ) by SEQ_4:20;
lim (NAT --> 1x) <= lim (() ^\ 1) by ;
then lim (NAT --> 1x) <= Sum () by ;
hence 1 + x <= exp_R . x by ; :: 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 S1[ 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) / () by SIN_COS:def 5
.= 1 by ;
then A22: S1[ 0 ] by ;
A23: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A24: S1[k] ; :: thesis: S1[k + 1]
per cases ( k is even or k is odd ) ;
suppose k is even ; :: thesis: S1[k + 1]
then consider m being Nat such that
A25: k = 2 * m by ABIAN:def 2;
k in NAT by ORDINAL1:def 12;
then A26: 1 - x <= (Partial_Sums ((- x) rExpSeq)) . (k + 1) by ;
A27: for k being Element of NAT st k is even & k > 0 holds
for y being Real holds () . k >= 0
proof
let k be Element of NAT ; :: thesis: ( k is even & k > 0 implies for y being Real holds () . k >= 0 )
assume that
A28: k is even and
A29: k > 0 ; :: thesis: for y being Real holds () . k >= 0
let y be Real; :: thesis: () . k >= 0
per cases ( y > 0 or y = 0 or y < 0 ) ;
suppose A31: y < 0 ; :: thesis: () . k >= 0
consider m being Nat such that
A32: k = 2 * m by ;
y |^ k = y |^ (m + m) by A32;
then y |^ k = (y |^ m) * (y |^ m) by NEWTON:8;
then A33: y |^ k = (y * y) |^ m by NEWTON:7;
y |^ k >= 0 by ;
then (y |^ k) / (k !) >= 0 ;
hence (y rExpSeq) . k >= 0 by SIN_COS:def 5; :: thesis: verum
end;
end;
end;
A34: ((- x) rExpSeq) . (k + 2) >= 0 by ;
A35: (Partial_Sums ((- x) rExpSeq)) . (k + 1) <= ((Partial_Sums ((- x) rExpSeq)) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) by ;
1 - x <= ((Partial_Sums ((- x) rExpSeq)) . (k + 1)) + (((- x) rExpSeq) . ((k + 1) + 1)) by ;
then 1 - x <= (Partial_Sums ((- x) rExpSeq)) . (k + 2) by SERIES_1:def 1;
hence S1[k + 1] ; :: thesis: verum
end;
suppose k is odd ; :: thesis: S1[k + 1]
then consider m being Nat such that
A36: k = (2 * m) + 1 by ABIAN:9;
A37: 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 S2[ 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) / () by SIN_COS:def 5
.= 1 by ;
((- x) rExpSeq) . 1 = ((- x) |^ 1) / (1 !) by SIN_COS:def 5;
then A43: ((- x) rExpSeq) . (1 + 0) = - x by NEWTON:13;
A44: S2[ 0 ] by ;
A45: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A46: S2[k] ; :: thesis: S2[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 ;
hence (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 1) <= (Partial_Sums ((- x) rExpSeq)) . ((2 * k) + 3) by ; :: thesis: verum
end;
hence S2[k + 1] by ; :: thesis: verum
end;
A48: for k being Nat holds S2[k] from consider m being Nat such that
A49: k = (2 * m) + 1 by ;
thus 1 - x <= (Partial_Sums ((- x) rExpSeq)) . k by ; :: thesis: verum
end;
1 - x <= (Partial_Sums ((- x) rExpSeq)) . (k + 2) by A36, A17, A18, A37;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from 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 ;
(- x) rExpSeq is summable by SIN_COS:45;
then A52: Partial_Sums ((- x) rExpSeq) is convergent by SERIES_1:def 2;
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 ;
then lim (NAT --> 1x) <= Sum ((- x) rExpSeq) by ;
hence 1 - x <= exp_R . (- x) by ; :: thesis: verum
end;
hence 1 - (- x) <= exp_R . (- (- x)) by ; :: thesis: verum
end;
suppose A54: - x > 1 ; :: thesis: 1 - (- x) <= exp_R . (- (- x))
0 < exp_R . (- (- x)) by ;
hence 1 - (- x) <= exp_R . (- (- x)) by ; :: thesis: verum
end;
end;
end;
hence 1 + x <= exp_R . x ; :: thesis: verum
end;
end;