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 e. RR+ -> ( 1 + A ) < ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( A e. RR+ -> A e. CC )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 0nn0 
 |-  0 e. NN0
4 3 a1i 
 |-  ( A e. CC -> 0 e. NN0 )
5 1e0p1 
 |-  1 = ( 0 + 1 )
6 0z 
 |-  0 e. ZZ
7 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
8 7 eftval 
 |-  ( 0 e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` 0 ) = ( ( A ^ 0 ) / ( ! ` 0 ) ) )
9 3 8 ax-mp 
 |-  ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` 0 ) = ( ( A ^ 0 ) / ( ! ` 0 ) )
10 eft0val 
 |-  ( A e. CC -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = 1 )
11 9 10 syl5eq 
 |-  ( A e. CC -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` 0 ) = 1 )
12 6 11 seq1i 
 |-  ( A e. CC -> ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` 0 ) = 1 )
13 1nn0 
 |-  1 e. NN0
14 7 eftval 
 |-  ( 1 e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` 1 ) = ( ( A ^ 1 ) / ( ! ` 1 ) ) )
15 13 14 ax-mp 
 |-  ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` 1 ) = ( ( A ^ 1 ) / ( ! ` 1 ) )
16 fac1 
 |-  ( ! ` 1 ) = 1
17 16 oveq2i 
 |-  ( ( A ^ 1 ) / ( ! ` 1 ) ) = ( ( A ^ 1 ) / 1 )
18 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
19 18 oveq1d 
 |-  ( A e. CC -> ( ( A ^ 1 ) / 1 ) = ( A / 1 ) )
20 div1 
 |-  ( A e. CC -> ( A / 1 ) = A )
21 19 20 eqtrd 
 |-  ( A e. CC -> ( ( A ^ 1 ) / 1 ) = A )
22 17 21 syl5eq 
 |-  ( A e. CC -> ( ( A ^ 1 ) / ( ! ` 1 ) ) = A )
23 15 22 syl5eq 
 |-  ( A e. CC -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` 1 ) = A )
24 2 4 5 12 23 seqp1d 
 |-  ( A e. CC -> ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` 1 ) = ( 1 + A ) )
25 1 24 syl 
 |-  ( A e. RR+ -> ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` 1 ) = ( 1 + A ) )
26 id 
 |-  ( A e. RR+ -> A e. RR+ )
27 13 a1i 
 |-  ( A e. RR+ -> 1 e. NN0 )
28 7 26 27 effsumlt 
 |-  ( A e. RR+ -> ( seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) ` 1 ) < ( exp ` A ) )
29 25 28 eqbrtrrd 
 |-  ( A e. RR+ -> ( 1 + A ) < ( exp ` A ) )