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	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
5		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
6		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
7	6	eftval	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(k\right)=\frac{A^k}{k!}$$
8	7	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(k\right)=\frac{A^k}{k!}$$
9		reeftcl	$$⊢\left(A\in ℝ\wedge k\in {\mathbb{N}}_0\right)\to \frac{A^k}{k!}\in ℝ$$
10	1 9	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{A^k}{k!}\in ℝ$$
11		oveq2	$$⊢n=k\to A^n=A^k$$
12		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼A^n\right)=\left(n\in {\mathbb{N}}_0⟼A^n\right)$$
13		ovex	$$⊢A^k\in \mathrm{V}$$
14	11 12 13	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
15	14	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
16		reexpcl	$$⊢\left(A\in ℝ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℝ$$
17	1 16	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℝ$$
18		faccl	$$⊢k\in {\mathbb{N}}_0\to k!\in \mathbb{N}$$
19	18	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k!\in \mathbb{N}$$
20	19	nnred	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k!\in ℝ$$
21	1	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\in ℝ$$
22		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
23	2	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 0\le A$$
24	21 22 23	expge0d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 0\le A^k$$
25	19	nnge1d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1\le k!$$
26	17 20 24 25	lemulge12d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A^k\le k!A^k$$
27	19	nngt0d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_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\leftrightarrow A^k\le k!A^k\right)$$
29	17 17 20 27 28	syl112anc	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\frac{A^k}{k!}\le A^k\leftrightarrow A^k\le k!A^k\right)$$
30	26 29	mpbird	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_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 {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\in \mathrm{dom}⇝$$
33	31 32	syl	$$⊢\phi \to seq0\left(+,\left(n\in {\mathbb{N}}_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 {\mathbb{N}}_0⟼A^n\right)\right)⇝\left(\frac{1}{1-A}\right)$$
37		seqex	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_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 {\mathbb{N}}_0⟼A^n\right)\right)⇝\left(\frac{1}{1-A}\right)\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝$$
40	36 39	syl	$$⊢\phi \to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)\in \mathrm{dom}⇝$$
41	4 5 8 10 15 17 30 33 40	isumle	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)\le \sum _{k\in {\mathbb{N}}_0}{A}^k$$
42		efval	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
43	31 42	syl	$$⊢\phi \to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
44		expcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
45	31 44	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
46	4 5 15 45 36	isumclim	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}{A}^k=\frac{1}{1-A}$$
47	46	eqcomd	$$⊢\phi \to \frac{1}{1-A}=\sum _{k\in {\mathbb{N}}_0}{A}^k$$
48	41 43 47	3brtr4d	$$⊢\phi \to {\mathrm{e}}^A\le \frac{1}{1-A}$$