# 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 ${⊢}{\phi }\to {A}\in ℝ$
eflegeo.2 ${⊢}{\phi }\to 0\le {A}$
eflegeo.3 ${⊢}{\phi }\to {A}<1$
Assertion eflegeo ${⊢}{\phi }\to {\mathrm{e}}^{{A}}\le \frac{1}{1-{A}}$

### Proof

Step Hyp Ref Expression
1 eflegeo.1 ${⊢}{\phi }\to {A}\in ℝ$
2 eflegeo.2 ${⊢}{\phi }\to 0\le {A}$
3 eflegeo.3 ${⊢}{\phi }\to {A}<1$
4 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
5 0zd ${⊢}{\phi }\to 0\in ℤ$
6 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)$
7 6 eftval ${⊢}{k}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
8 7 adantl ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
9 reeftcl ${⊢}\left({A}\in ℝ\wedge {k}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{k}}}{{k}!}\in ℝ$
10 1 9 sylan ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{k}}}{{k}!}\in ℝ$
11 oveq2 ${⊢}{n}={k}\to {{A}}^{{n}}={{A}}^{{k}}$
12 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)=\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)$
13 ovex ${⊢}{{A}}^{{k}}\in \mathrm{V}$
14 11 12 13 fvmpt ${⊢}{k}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({k}\right)={{A}}^{{k}}$
15 14 adantl ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({k}\right)={{A}}^{{k}}$
16 reexpcl ${⊢}\left({A}\in ℝ\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℝ$
17 1 16 sylan ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℝ$
18 faccl ${⊢}{k}\in {ℕ}_{0}\to {k}!\in ℕ$
19 18 adantl ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {k}!\in ℕ$
20 19 nnred ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {k}!\in ℝ$
21 1 adantr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {A}\in ℝ$
22 simpr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
23 2 adantr ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to 0\le {A}$
24 21 22 23 expge0d ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to 0\le {{A}}^{{k}}$
25 19 nnge1d ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to 1\le {k}!$
26 17 20 24 25 lemulge12d ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\le {k}!{{A}}^{{k}}$
27 19 nngt0d ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to 0<{k}!$
28 ledivmul ${⊢}\left({{A}}^{{k}}\in ℝ\wedge {{A}}^{{k}}\in ℝ\wedge \left({k}!\in ℝ\wedge 0<{k}!\right)\right)\to \left(\frac{{{A}}^{{k}}}{{k}!}\le {{A}}^{{k}}↔{{A}}^{{k}}\le {k}!{{A}}^{{k}}\right)$
29 17 17 20 27 28 syl112anc ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \left(\frac{{{A}}^{{k}}}{{k}!}\le {{A}}^{{k}}↔{{A}}^{{k}}\le {k}!{{A}}^{{k}}\right)$
30 26 29 mpbird ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{k}}}{{k}!}\le {{A}}^{{k}}$
31 1 recnd ${⊢}{\phi }\to {A}\in ℂ$
32 6 efcllem ${⊢}{A}\in ℂ\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\in \mathrm{dom}⇝$
33 31 32 syl ${⊢}{\phi }\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)\right)\in \mathrm{dom}⇝$
34 1 2 absidd ${⊢}{\phi }\to \left|{A}\right|={A}$
35 34 3 eqbrtrd ${⊢}{\phi }\to \left|{A}\right|<1$
36 31 35 15 geolim ${⊢}{\phi }\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\right)⇝\left(\frac{1}{1-{A}}\right)$
37 seqex ${⊢}seq0\left(+,\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\right)\in \mathrm{V}$
38 ovex ${⊢}\frac{1}{1-{A}}\in \mathrm{V}$
39 37 38 breldm ${⊢}seq0\left(+,\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\right)⇝\left(\frac{1}{1-{A}}\right)\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\right)\in \mathrm{dom}⇝$
40 36 39 syl ${⊢}{\phi }\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\right)\in \mathrm{dom}⇝$
41 4 5 8 10 15 17 30 33 40 isumle ${⊢}{\phi }\to \sum _{{k}\in {ℕ}_{0}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)\le \sum _{{k}\in {ℕ}_{0}}{{A}}^{{k}}$
42 efval ${⊢}{A}\in ℂ\to {\mathrm{e}}^{{A}}=\sum _{{k}\in {ℕ}_{0}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
43 31 42 syl ${⊢}{\phi }\to {\mathrm{e}}^{{A}}=\sum _{{k}\in {ℕ}_{0}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
44 expcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℂ$
45 31 44 sylan ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℂ$
46 4 5 15 45 36 isumclim ${⊢}{\phi }\to \sum _{{k}\in {ℕ}_{0}}{{A}}^{{k}}=\frac{1}{1-{A}}$
47 46 eqcomd ${⊢}{\phi }\to \frac{1}{1-{A}}=\sum _{{k}\in {ℕ}_{0}}{{A}}^{{k}}$
48 41 43 47 3brtr4d ${⊢}{\phi }\to {\mathrm{e}}^{{A}}\le \frac{1}{1-{A}}$