# 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 ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. NN )`
20 19 nnred
` |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. RR )`
` |-  ( ( ph /\ k e. NN0 ) -> A e. RR )`
22 simpr
` |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )`
` |-  ( ( 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 ) ) )`