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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpcn | |
|
2 | nn0uz | |
|
3 | 0nn0 | |
|
4 | 3 | a1i | |
5 | 1e0p1 | |
|
6 | 0z | |
|
7 | eqid | |
|
8 | 7 | eftval | |
9 | 3 8 | ax-mp | |
10 | eft0val | |
|
11 | 9 10 | eqtrid | |
12 | 6 11 | seq1i | |
13 | 1nn0 | |
|
14 | 7 | eftval | |
15 | 13 14 | ax-mp | |
16 | fac1 | |
|
17 | 16 | oveq2i | |
18 | exp1 | |
|
19 | 18 | oveq1d | |
20 | div1 | |
|
21 | 19 20 | eqtrd | |
22 | 17 21 | eqtrid | |
23 | 15 22 | eqtrid | |
24 | 2 4 5 12 23 | seqp1d | |
25 | 1 24 | syl | |
26 | id | |
|
27 | 13 | a1i | |
28 | 7 26 27 | effsumlt | |
29 | 25 28 | eqbrtrrd | |