A1: number_e is irrational by IRRAT_1:41;
A2: 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:3 ; :: 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:9; :: thesis: ( th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A3: th |^ 1 = (th GeoSeq) . (0 + 1) by PREPOWER:def 1
.= ((th GeoSeq) . 0) * th by PREPOWER:3
.= 1 * th by PREPOWER:3
.= th ; :: thesis: ( th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ 2 = th |^ (1 + 1)
.= th * th by A3, NEWTON:8 ; :: thesis: ( (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A4: (- 1) |^ (2 * n) = 1 |^ (2 * n) by POWER:1
.= 1 by NEWTON:10 ; :: thesis: (- 1) |^ ((2 * n) + 1) = - 1
thus (- 1) |^ ((2 * n) + 1) = ((- 1) |^ (2 * n)) * (- 1) by NEWTON:6
.= - 1 by A4 ; :: thesis: verum

end;

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 ;
( 1 |^ (n + 1) > 0 & (n + 1) ! > 0 ) by PREPOWER:6;
then 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 A2, NEWTON:12
.= 1 + (1 / 1) by A2, 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 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 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