A1: number_e is irrational by IRRAT_1:41;
A5: for n being Element of NAT st 1 <= n holds
() . n >= 2
proof
defpred S1[ Integer] means () . \$1 >= 2;
A6: for ni being Integer st 1 <= ni & S1[ni] holds
S1[ni + 1]
proof
let ni be Integer; :: thesis: ( 1 <= ni & S1[ni] implies S1[ni + 1] )
assume 1 <= ni ; :: thesis: ( not S1[ni] or S1[ni + 1] )
then reconsider n = ni as Element of NAT by INT_1:3;
A7: () . (n + 1) = (() . n) + (() . (n + 1)) by SERIES_1:def 1
.= (() . n) + ((1 |^ (n + 1)) / ((n + 1) !)) by SIN_COS:def 5 ;
A8: ((Partial_Sums ()) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) > () . n by ;
assume (Partial_Sums ()) . ni >= 2 ; :: thesis: S1[ni + 1]
hence S1[ni + 1] by ; :: thesis: verum
end;
() . 1 = (() . 0) + (() . (0 + 1)) by SERIES_1:def 1
.= (() . 0) + (() . 1) by SERIES_1:def 1
.= (() . 0) + ((1 |^ 1) / (1 !)) by SIN_COS:def 5
.= ((1 |^ 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: S1 ;
for n being Integer st 1 <= n holds
S1[n] from INT_1:sch 2(A9, A6);
hence for n being Element of NAT st 1 <= n holds
() . n >= 2 ; :: thesis: verum
end;
A10: for n being Nat holds (() ^\ 1) . n >= 2
proof
let n be Nat; :: thesis: (() ^\ 1) . n >= 2
((Partial_Sums ()) ^\ 1) . n = () . (n + 1) by NAT_1:def 3;
hence ((Partial_Sums ()) ^\ 1) . n >= 2 by ; :: thesis: verum
end;
1 rExpSeq is summable by SIN_COS:45;
then A11: Partial_Sums () is convergent by SERIES_1:def 2;
lim () = Sum () by SERIES_1:def 3;
then lim (() ^\ 1) = Sum () by ;
then Sum () >= 2 by ;
then exp_R . 1 >= 2 by SIN_COS:def 22;
then number_e >= 2 by ;
then ( number_e > 2 or number_e = 2 ) by XXREAL_0:1;
hence number_e > 2 by A1; :: thesis: verum