A0: number_e is irrational by IRRAT_1:42;
A1: for th, th1, th2, th3 being real number
for n being Element of NAT holds
( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )

proof

let th, th1, th2, th3 be real number ; :: thesis: for n being Element of NAT holds
( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
let n be Element of NAT ; :: thesis: ( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ 0 = (th GeoSeq) . 0 by PREPOWER:def 1
.= 1 by PREPOWER:4 ; :: thesis: ( th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ (2 * n) = (th |^ n) |^ 2 by NEWTON:14; :: thesis: ( th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A2: th |^ 1 = (th GeoSeq) . (0 + 1) by PREPOWER:def 1
.= ((th GeoSeq) . 0) * th by PREPOWER:4
.= 1 * th by PREPOWER:4
.= th ; :: thesis: ( th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ 2 = th |^ (1 + 1)
.= th * th by A2, NEWTON:13 ; :: thesis: ( (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A3: (- 1) |^ (2 * n) = 1 |^ (2 * n) by POWER:1
.= 1 by NEWTON:15 ; :: thesis: (- 1) |^ ((2 * n) + 1) = - 1
thus (- 1) |^ ((2 * n) + 1) = ((- 1) |^ (2 * n)) * (- 1) by NEWTON:11
.= - 1 by A3 ; :: thesis: verum

end;

A4: 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;
A5: 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:16;
A6: (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 9 ;
( 1 |^ (n + 1) > 0 & (n + 1) ! > 0 ) by PREPOWER:13;
then A7: ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) > (Partial_Sums (1 rExpSeq)) . n by XREAL_1:31, XREAL_1:141;
assume (Partial_Sums (1 rExpSeq)) . ni >= 2 ; :: thesis: S₁[ni + 1]
hence S₁[ni + 1] by A6, A7, 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 9
.= ((1 |^ 0) / (0 !)) + ((1 |^ 1) / (1 !)) by SIN_COS:def 9
.= 1 + ((1 |^ 1) / (1 !)) by A1, NEWTON:18
.= 1 + (1 / 1) by A1, NEWTON:19
.= 2 ;
then A8: S₁[1] ;
for n being Integer st 1 <= n holds
S₁[n] from INT_1:sch 2(A8, A5);
hence for n being Element of NAT st 1 <= n holds
(Partial_Sums (1 rExpSeq)) . n >= 2 ; :: thesis: verum

end;

A9: for n being Element of NAT holds ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2

proof

let n be Element of 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 A4, NAT_1:11; :: thesis: verum

end;

1 rExpSeq is summable by SIN_COS:49;
then A10: 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 A10, SEQ_4:33;
then Sum (1 rExpSeq) >= 2 by A9, A10, SIN_COS:41;
then exp_R . 1 >= 2 by SIN_COS:def 26;
then number_e >= 2 by IRRAT_1:def 7, SIN_COS:def 27;
then ( number_e > 2 or number_e = 2 ) by XXREAL_0:1;
hence number_e > 2 by A0; :: thesis: verum