Theorem efgt1p

Description: The exponential of a positive real number is greater than 1 plus that number. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Assertion	efgt1p	$$⊢A\in {ℝ}^{+}\to 1+A<{\mathrm{e}}^A$$

Proof

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