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;
A3: (Partial_Sums (th rExpSeq )) . 0 = (th rExpSeq ) . 0 by SERIES_1:def 1
.= (th |^ 0 ) / (0 ! ) by Def9
.= 1 by NEWTON:9, NEWTON:18 ;
A4: S₁[ 0 ] by A3;
A5: 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 A6: (Partial_Sums (th rExpSeq )) . n >= 1 ; :: thesis: S₁[n + 1]
A7: (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 ;
A8: ( th |^ (n + 1) > 0 & (n + 1) ! > 0 ) by A1, NEWTON:23, PREPOWER:13;
A9: ((Partial_Sums (th rExpSeq )) . n) + ((th |^ (n + 1)) / ((n + 1) ! )) > (Partial_Sums (th rExpSeq )) . n by A8, XREAL_1:31;
thus S₁[n + 1] by A6, A7, A9, XXREAL_0:2; :: thesis: verum

end;

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

end;

A11: th is Real by XREAL_0:def 1;
A12: th rExpSeq is summable by A11, Th49;
A13: Partial_Sums (th rExpSeq ) is convergent by A12, SERIES_1:def 2;
A14: lim (Partial_Sums (th rExpSeq )) = Sum (th rExpSeq ) by SERIES_1:def 3;
A15: Sum (th rExpSeq ) >= 1 by A2, A13, A14, PREPOWER:2;
thus exp_R . th >= 1 by A15, Def26; :: thesis: verum