Metamath Proof Explorer

Theorem efgt1p2

Description: The exponential of a positive real number is greater than the sum of the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion efgt1p2 
|- ( A e. RR+ -> ( ( 1 + A ) + ( ( A ^ 2 ) / 2 ) ) < ( exp ` A ) )

Proof

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