A1:
number_e is irrational
by IRRAT_1:41;

A5: for n being Element of NAT st 1 <= n holds

(Partial_Sums (1 rExpSeq)) . n >= 2

then A11: Partial_Sums (1 rExpSeq) is convergent by SERIES_1:def 2;

lim (Partial_Sums (1 rExpSeq)) = Sum (1 rExpSeq) by SERIES_1:def 3;

then lim ((Partial_Sums (1 rExpSeq)) ^\ 1) = Sum (1 rExpSeq) by A11, SEQ_4:20;

then Sum (1 rExpSeq) >= 2 by A10, A11, SIN_COS:38;

then exp_R . 1 >= 2 by SIN_COS:def 22;

then number_e >= 2 by IRRAT_1:def 7, SIN_COS:def 23;

then ( number_e > 2 or number_e = 2 ) by XXREAL_0:1;

hence number_e > 2 by A1; :: thesis: verum

A5: for n being Element of NAT st 1 <= n holds

(Partial_Sums (1 rExpSeq)) . n >= 2

proof

A10:
for n being Nat holds ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2
defpred S_{1}[ Integer] means (Partial_Sums (1 rExpSeq)) . $1 >= 2;

A6: for ni being Integer st 1 <= ni & S_{1}[ni] holds

S_{1}[ni + 1]

.= ((1 rExpSeq) . 0) + ((1 rExpSeq) . 1) by SERIES_1:def 1

.= ((1 rExpSeq) . 0) + ((1 |^ 1) / (1 !)) by SIN_COS:def 5

.= ((1 |^ 0) / (0 !)) + ((1 |^ 1) / (1 !)) by SIN_COS:def 5

.= 1 + ((1 |^ 1) / (1 !)) by NEWTON:12

.= 1 + (1 / 1) by NEWTON:13

.= 2 ;

then A9: S_{1}[1]
;

for n being Integer st 1 <= n holds

S_{1}[n]
from INT_1:sch 2(A9, A6);

hence for n being Element of NAT st 1 <= n holds

(Partial_Sums (1 rExpSeq)) . n >= 2 ; :: thesis: verum

end;A6: for ni being Integer st 1 <= ni & S

S

proof

(Partial_Sums (1 rExpSeq)) . 1 =
((Partial_Sums (1 rExpSeq)) . 0) + ((1 rExpSeq) . (0 + 1))
by SERIES_1:def 1
let ni be Integer; :: thesis: ( 1 <= ni & S_{1}[ni] implies S_{1}[ni + 1] )

assume 1 <= ni ; :: thesis: ( not S_{1}[ni] or S_{1}[ni + 1] )

then reconsider n = ni as Element of NAT by INT_1:3;

A7: (Partial_Sums (1 rExpSeq)) . (n + 1) = ((Partial_Sums (1 rExpSeq)) . n) + ((1 rExpSeq) . (n + 1)) by SERIES_1:def 1

.= ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) by SIN_COS:def 5 ;

A8: ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) > (Partial_Sums (1 rExpSeq)) . n by XREAL_1:29, XREAL_1:139;

assume (Partial_Sums (1 rExpSeq)) . ni >= 2 ; :: thesis: S_{1}[ni + 1]

hence S_{1}[ni + 1]
by A7, A8, XXREAL_0:2; :: thesis: verum

end;assume 1 <= ni ; :: thesis: ( not S

then reconsider n = ni as Element of NAT by INT_1:3;

A7: (Partial_Sums (1 rExpSeq)) . (n + 1) = ((Partial_Sums (1 rExpSeq)) . n) + ((1 rExpSeq) . (n + 1)) by SERIES_1:def 1

.= ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) by SIN_COS:def 5 ;

A8: ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) > (Partial_Sums (1 rExpSeq)) . n by XREAL_1:29, XREAL_1:139;

assume (Partial_Sums (1 rExpSeq)) . ni >= 2 ; :: thesis: S

hence S

.= ((1 rExpSeq) . 0) + ((1 rExpSeq) . 1) by SERIES_1:def 1

.= ((1 rExpSeq) . 0) + ((1 |^ 1) / (1 !)) by SIN_COS:def 5

.= ((1 |^ 0) / (0 !)) + ((1 |^ 1) / (1 !)) by SIN_COS:def 5

.= 1 + ((1 |^ 1) / (1 !)) by NEWTON:12

.= 1 + (1 / 1) by NEWTON:13

.= 2 ;

then A9: S

for n being Integer st 1 <= n holds

S

hence for n being Element of NAT st 1 <= n holds

(Partial_Sums (1 rExpSeq)) . n >= 2 ; :: thesis: verum

proof

1 rExpSeq is summable
by SIN_COS:45;
let n be Nat; :: thesis: ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2

((Partial_Sums (1 rExpSeq)) ^\ 1) . n = (Partial_Sums (1 rExpSeq)) . (n + 1) by NAT_1:def 3;

hence ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2 by A5, NAT_1:11; :: thesis: verum

end;((Partial_Sums (1 rExpSeq)) ^\ 1) . n = (Partial_Sums (1 rExpSeq)) . (n + 1) by NAT_1:def 3;

hence ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2 by A5, NAT_1:11; :: thesis: verum

then A11: Partial_Sums (1 rExpSeq) is convergent by SERIES_1:def 2;

lim (Partial_Sums (1 rExpSeq)) = Sum (1 rExpSeq) by SERIES_1:def 3;

then lim ((Partial_Sums (1 rExpSeq)) ^\ 1) = Sum (1 rExpSeq) by A11, SEQ_4:20;

then Sum (1 rExpSeq) >= 2 by A10, A11, SIN_COS:38;

then exp_R . 1 >= 2 by SIN_COS:def 22;

then number_e >= 2 by IRRAT_1:def 7, SIN_COS:def 23;

then ( number_e > 2 or number_e = 2 ) by XXREAL_0:1;

hence number_e > 2 by A1; :: thesis: verum