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

proof

defpred S₁[ Integer] means (Partial_Sums (1 rExpSeq)) . $1 >= 2;
A6: for ni being Integer st 1 <= ni & S₁[ni] holds
S₁[ni + 1]

proof

let ni be Integer; :: thesis: ( 1 <= ni & S₁[ni] implies S₁[ni + 1] )
assume 1 <= ni ; :: thesis: ( not S₁[ni] or S₁[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₁[ni + 1]
hence S₁[ni + 1] by A7, A8, XXREAL_0:2; :: thesis: verum

end;

(Partial_Sums (1 rExpSeq)) . 1 = ((Partial_Sums (1 rExpSeq)) . 0) + ((1 rExpSeq) . (0 + 1)) by SERIES_1:def 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] ;
for n being Integer st 1 <= n holds
S₁[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;

A10: for n being Nat holds ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2

proof

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;

1 rExpSeq is summable by SIN_COS:45;
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