let th be real number ; :: thesis: ( th > 0 implies exp_R . th >= 1 )
assume A1: th > 0 ; :: thesis: exp_R . th >= 1
A2: for n being Element of NAT holds (Partial_Sums (th rExpSeq )) . n >= 1

proof

defpred S₁[ Element of 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 Def9
.= 1 by NEWTON:9, NEWTON:18 ;
then A3: S₁[ 0 ] ;
A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: (Partial_Sums (th rExpSeq )) . n >= 1 ; :: thesis: S₁[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 Def9 ;
A7: th |^ (n + 1) > 0 by A1, PREPOWER:13;
(n + 1) ! > 0 by NEWTON:23;
then ((Partial_Sums (th rExpSeq )) . n) + ((th |^ (n + 1)) / ((n + 1) ! )) > (Partial_Sums (th rExpSeq )) . n by A7, XREAL_1:31;
hence S₁[n + 1] by A5, A6, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
hence for n being Element of NAT holds (Partial_Sums (th rExpSeq )) . n >= 1 ; :: thesis: verum

end;

th is Real by XREAL_0:def 1;
then th rExpSeq is summable by Th49;
then ( Partial_Sums (th rExpSeq ) is convergent & lim (Partial_Sums (th rExpSeq )) = Sum (th rExpSeq ) ) by SERIES_1:def 2, SERIES_1:def 3;
then Sum (th rExpSeq ) >= 1 by A2, PREPOWER:2;
hence exp_R . th >= 1 by Def26; :: thesis: verum