Metamath Proof Explorer

Theorem eflegeo

Description: The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007)

Ref Expression
Hypotheses eflegeo.1 
|- ( ph -> A e. RR )
eflegeo.2 
|- ( ph -> 0 <_ A )
eflegeo.3 
|- ( ph -> A < 1 )
Assertion eflegeo 
|- ( ph -> ( exp ` A ) <_ ( 1 / ( 1 - A ) ) )

Proof

Step Hyp Ref Expression
1 eflegeo.1 
 |-  ( ph -> A e. RR )
2 eflegeo.2 
 |-  ( ph -> 0 <_ A )
3 eflegeo.3 
 |-  ( ph -> A < 1 )
4 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
5 0zd 
 |-  ( ph -> 0 e. ZZ )
6 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
7 6 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
8 7 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
9 reeftcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
10 1 9 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
11 oveq2 
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
12 eqid 
 |-  ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
13 ovex 
 |-  ( A ^ k ) e. _V
14 11 12 13 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
15 14 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
16 reexpcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( A ^ k ) e. RR )
17 1 16 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ^ k ) e. RR )
18 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
19 18 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. NN )
20 19 nnred 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. RR )
21 1 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> A e. RR )
22 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
23 2 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ A )
24 21 22 23 expge0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 <_ ( A ^ k ) )
25 19 nnge1d 
 |-  ( ( ph /\ k e. NN0 ) -> 1 <_ ( ! ` k ) )
26 17 20 24 25 lemulge12d 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ^ k ) <_ ( ( ! ` k ) x. ( A ^ k ) ) )
27 19 nngt0d 
 |-  ( ( ph /\ k e. NN0 ) -> 0 < ( ! ` k ) )
28 ledivmul 
 |-  ( ( ( A ^ k ) e. RR /\ ( A ^ k ) e. RR /\ ( ( ! ` k ) e. RR /\ 0 < ( ! ` k ) ) ) -> ( ( ( A ^ k ) / ( ! ` k ) ) <_ ( A ^ k ) <-> ( A ^ k ) <_ ( ( ! ` k ) x. ( A ^ k ) ) ) )
29 17 17 20 27 28 syl112anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( A ^ k ) / ( ! ` k ) ) <_ ( A ^ k ) <-> ( A ^ k ) <_ ( ( ! ` k ) x. ( A ^ k ) ) ) )
30 26 29 mpbird 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) <_ ( A ^ k ) )
31 1 recnd 
 |-  ( ph -> A e. CC )
32 6 efcllem 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
33 31 32 syl 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
34 1 2 absidd 
 |-  ( ph -> ( abs ` A ) = A )
35 34 3 eqbrtrd 
 |-  ( ph -> ( abs ` A ) < 1 )
36 31 35 15 geolim 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) )
37 seqex 
 |-  seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. _V
38 ovex 
 |-  ( 1 / ( 1 - A ) ) e. _V
39 37 38 breldm 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
40 36 39 syl 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
41 4 5 8 10 15 17 30 33 40 isumle 
 |-  ( ph -> sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) <_ sum_ k e. NN0 ( A ^ k ) )
42 efval 
 |-  ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
43 31 42 syl 
 |-  ( ph -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
44 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
45 31 44 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ^ k ) e. CC )
46 4 5 15 45 36 isumclim 
 |-  ( ph -> sum_ k e. NN0 ( A ^ k ) = ( 1 / ( 1 - A ) ) )
47 46 eqcomd 
 |-  ( ph -> ( 1 / ( 1 - A ) ) = sum_ k e. NN0 ( A ^ k ) )
48 41 43 47 3brtr4d 
 |-  ( ph -> ( exp ` A ) <_ ( 1 / ( 1 - A ) ) )