let th be Real; :: thesis: ( th > 0 implies exp_R . th >= 1 )
assume A1: th > 0 ; :: thesis: exp_R . th >= 1
A2: for n being Nat holds (Partial_Sums (th rExpSeq)) . n >= 1
proof
defpred S1[ Nat] means (Partial_Sums (th rExpSeq)) . $1 >= 1;
(Partial_Sums (th rExpSeq)) . 0 = (th rExpSeq) . 0 by SERIES_1:def 1
.= (th |^ 0) / (0 !) by Def5
.= 1 by NEWTON:4, NEWTON:12 ;
then A3: S1[ 0 ] ;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: (Partial_Sums (th rExpSeq)) . n >= 1 ; :: thesis: S1[n + 1]
A6: (Partial_Sums (th rExpSeq)) . (n + 1) = ((Partial_Sums (th rExpSeq)) . n) + ((th rExpSeq) . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums (th rExpSeq)) . n) + ((th |^ (n + 1)) / ((n + 1) !)) by Def5 ;
( th |^ (n + 1) > 0 & (n + 1) ! > 0 ) by A1, PREPOWER:6;
then ((Partial_Sums (th rExpSeq)) . n) + ((th |^ (n + 1)) / ((n + 1) !)) > (Partial_Sums (th rExpSeq)) . n by XREAL_1:29;
hence S1[n + 1] by A5, A6, XXREAL_0:2; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
 hence for n being Nat holds (Partial_Sums (th rExpSeq)) . n >= 1 ; :: thesis: verum
end;
th rExpSeq is summable by Th44;
then A7: Partial_Sums (th rExpSeq) is convergent by SERIES_1:def 2;
lim (Partial_Sums (th rExpSeq)) = Sum (th rExpSeq) by SERIES_1:def 3;
then Sum (th rExpSeq) >= 1 by A2, A7, PREPOWER:1;
hence exp_R . th >= 1 by Def22; :: thesis: verum