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\in {ℝ}^{+}\to 1+A+\left(\frac{A^2}{2}\right)<{\mathrm{e}}^A$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3	2	a1i	$$⊢A\in {ℝ}^{+}\to 1\in {\mathbb{N}}_0$$
4		df-2	$$⊢2=1+1$$
5		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7	6	a1i	$$⊢A\in ℂ\to 0\in {\mathbb{N}}_0$$
8		1e0p1	$$⊢1=0+1$$
9		0z	$$⊢0\in \mathbb{Z}$$
10		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
11	10	eftval	$$⊢0\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(0\right)=\frac{A^0}{0!}$$
12	6 11	ax-mp	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(0\right)=\frac{A^0}{0!}$$
13		eft0val	$$⊢A\in ℂ\to \frac{A^0}{0!}=1$$
14	12 13	syl5eq	$$⊢A\in ℂ\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(0\right)=1$$
15	9 14	seq1i	$$⊢A\in ℂ\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\left(0\right)=1$$
16	10	eftval	$$⊢1\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(1\right)=\frac{A^1}{1!}$$
17	2 16	ax-mp	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(1\right)=\frac{A^1}{1!}$$
18		fac1	$$⊢1!=1$$
19	18	oveq2i	$$⊢\frac{A^1}{1!}=\frac{A^1}{1}$$
20		exp1	$$⊢A\in ℂ\to A^1=A$$
21	20	oveq1d	$$⊢A\in ℂ\to \frac{A^1}{1}=\frac{A}{1}$$
22		div1	$$⊢A\in ℂ\to \frac{A}{1}=A$$
23	21 22	eqtrd	$$⊢A\in ℂ\to \frac{A^1}{1}=A$$
24	19 23	syl5eq	$$⊢A\in ℂ\to \frac{A^1}{1!}=A$$
25	17 24	syl5eq	$$⊢A\in ℂ\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(1\right)=A$$
26	1 7 8 15 25	seqp1d	$$⊢A\in ℂ\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\left(1\right)=1+A$$
27	5 26	syl	$$⊢A\in {ℝ}^{+}\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\left(1\right)=1+A$$
28		2nn0	$$⊢2\in {\mathbb{N}}_0$$
29	10	eftval	$$⊢2\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(2\right)=\frac{A^2}{2!}$$
30	28 29	ax-mp	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(2\right)=\frac{A^2}{2!}$$
31		fac2	$$⊢2!=2$$
32	31	oveq2i	$$⊢\frac{A^2}{2!}=\frac{A^2}{2}$$
33	30 32	eqtri	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(2\right)=\frac{A^2}{2}$$
34	33	a1i	$$⊢A\in {ℝ}^{+}\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(2\right)=\frac{A^2}{2}$$
35	1 3 4 27 34	seqp1d	$$⊢A\in {ℝ}^{+}\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\left(2\right)=1+A+\left(\frac{A^2}{2}\right)$$
36		id	$$⊢A\in {ℝ}^{+}\to A\in {ℝ}^{+}$$
37	28	a1i	$$⊢A\in {ℝ}^{+}\to 2\in {\mathbb{N}}_0$$
38	10 36 37	effsumlt	$$⊢A\in {ℝ}^{+}\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\left(2\right)<{\mathrm{e}}^A$$
39	35 38	eqbrtrrd	$$⊢A\in {ℝ}^{+}\to 1+A+\left(\frac{A^2}{2}\right)<{\mathrm{e}}^A$$