let x be Real; :: thesis: ( x > 0 implies exp_R . x > x + 1 )
assume AA: x > 0 ; :: thesis: exp_R . x > x + 1
set r = 1;
set f = Maclaurin (exp_R,].(- 1),1.[,x);
A4: exp_R . x = Sum (Maclaurin (exp_R,].(- 1),1.[,x)) by TAYLOR_2:16;
A2: (Maclaurin (exp_R,].(- 1),1.[,x)) . 0 = (x |^ 0) / (0 !) by TAYLOR_2:8
.= 1 by NEWTON:4, NEWTON:12 ;
A3: (Maclaurin (exp_R,].(- 1),1.[,x)) . 1 = (x |^ 1) / (1 !) by TAYLOR_2:8
.= x by NEWTON:13 ;
SS: Maclaurin (exp_R,].(- 1),1.[,x) is absolutely_summable by TAYLOR_2:16;
then A6: Sum (Maclaurin (exp_R,].(- 1),1.[,x)) = ((Partial_Sums (Maclaurin (exp_R,].(- 1),1.[,x))) . 1) + (Sum ((Maclaurin (exp_R,].(- 1),1.[,x)) ^\ (1 + 1))) by SERIES_1:15
.= (((Partial_Sums (Maclaurin (exp_R,].(- 1),1.[,x))) . 0) + ((Maclaurin (exp_R,].(- 1),1.[,x)) . (0 + 1))) + (Sum ((Maclaurin (exp_R,].(- 1),1.[,x)) ^\ (1 + 1))) by SERIES_1:def 1
.= (1 + x) + (Sum ((Maclaurin (exp_R,].(- 1),1.[,x)) ^\ (1 + 1))) by A2, A3, SERIES_1:def 1 ;
( Maclaurin (exp_R,].(- 1),1.[,x) is positive-yielding & Maclaurin (exp_R,].(- 1),1.[,x) is summable ) by MacPositive, AA, SS;
hence exp_R . x > x + 1 by A4, A6, XREAL_1:29, Th36; :: thesis: verum