Metamath Proof Explorer


Theorem efgt1p

Description: The exponential of a positive real number is greater than 1 plus that number. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion efgt1p A+1+A<eA

Proof

Step Hyp Ref Expression
1 rpcn A+A
2 nn0uz 0=0
3 0nn0 00
4 3 a1i A00
5 1e0p1 1=0+1
6 0z 0
7 eqid n0Ann!=n0Ann!
8 7 eftval 00n0Ann!0=A00!
9 3 8 ax-mp n0Ann!0=A00!
10 eft0val AA00!=1
11 9 10 eqtrid An0Ann!0=1
12 6 11 seq1i Aseq0+n0Ann!0=1
13 1nn0 10
14 7 eftval 10n0Ann!1=A11!
15 13 14 ax-mp n0Ann!1=A11!
16 fac1 1!=1
17 16 oveq2i A11!=A11
18 exp1 AA1=A
19 18 oveq1d AA11=A1
20 div1 AA1=A
21 19 20 eqtrd AA11=A
22 17 21 eqtrid AA11!=A
23 15 22 eqtrid An0Ann!1=A
24 2 4 5 12 23 seqp1d Aseq0+n0Ann!1=1+A
25 1 24 syl A+seq0+n0Ann!1=1+A
26 id A+A+
27 13 a1i A+10
28 7 26 27 effsumlt A+seq0+n0Ann!1<eA
29 25 28 eqbrtrrd A+1+A<eA