Theorem ef4p

Description: Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypothesis	ef4p.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
Assertion	ef4p	$$⊢A\in ℂ\to {\mathrm{e}}^A=\left(1+A+\left(\frac{A^2}{2}\right)\right)+\left(\frac{A^3}{6}\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$

Proof

Step	Hyp	Ref	Expression
1		ef4p.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		df-4	$$⊢4=3+1$$
3		3nn0	$$⊢3\in {\mathbb{N}}_0$$
4		id	$$⊢A\in ℂ\to A\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6		addcl	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to 1+A\in ℂ$$
7	5 6	mpan	$$⊢A\in ℂ\to 1+A\in ℂ$$
8		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
9	8	halfcld	$$⊢A\in ℂ\to \frac{A^2}{2}\in ℂ$$
10	7 9	addcld	$$⊢A\in ℂ\to 1+A+\left(\frac{A^2}{2}\right)\in ℂ$$
11		df-3	$$⊢3=2+1$$
12		2nn0	$$⊢2\in {\mathbb{N}}_0$$
13		df-2	$$⊢2=1+1$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	5	a1i	$$⊢A\in ℂ\to 1\in ℂ$$
16		1e0p1	$$⊢1=0+1$$
17		0nn0	$$⊢0\in {\mathbb{N}}_0$$
18		0cnd	$$⊢A\in ℂ\to 0\in ℂ$$
19	1	efval2	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}F\left(k\right)$$
20		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
21	20	sumeq1i	$$⊢\sum _{k\in {\mathbb{N}}_0}F\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge 0}}F\left(k\right)$$
22	19 21	syl6req	$$⊢A\in ℂ\to \sum _{k\in {\mathbb{Z}}_{\ge 0}}F\left(k\right)={\mathrm{e}}^A$$
23	22	oveq2d	$$⊢A\in ℂ\to 0+\sum _{k\in {\mathbb{Z}}_{\ge 0}}F\left(k\right)=0+{\mathrm{e}}^A$$
24		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
25	24	addid2d	$$⊢A\in ℂ\to 0+{\mathrm{e}}^A={\mathrm{e}}^A$$
26	23 25	eqtr2d	$$⊢A\in ℂ\to {\mathrm{e}}^A=0+\sum _{k\in {\mathbb{Z}}_{\ge 0}}F\left(k\right)$$
27		eft0val	$$⊢A\in ℂ\to \frac{A^0}{0!}=1$$
28	27	oveq2d	$$⊢A\in ℂ\to 0+\left(\frac{A^0}{0!}\right)=0+1$$
29		0p1e1	$$⊢0+1=1$$
30	28 29	syl6eq	$$⊢A\in ℂ\to 0+\left(\frac{A^0}{0!}\right)=1$$
31	1 16 17 4 18 26 30	efsep	$$⊢A\in ℂ\to {\mathrm{e}}^A=1+\sum _{k\in {\mathbb{Z}}_{\ge 1}}F\left(k\right)$$
32		exp1	$$⊢A\in ℂ\to A^1=A$$
33		fac1	$$⊢1!=1$$
34	33	a1i	$$⊢A\in ℂ\to 1!=1$$
35	32 34	oveq12d	$$⊢A\in ℂ\to \frac{A^1}{1!}=\frac{A}{1}$$
36		div1	$$⊢A\in ℂ\to \frac{A}{1}=A$$
37	35 36	eqtrd	$$⊢A\in ℂ\to \frac{A^1}{1!}=A$$
38	37	oveq2d	$$⊢A\in ℂ\to 1+\left(\frac{A^1}{1!}\right)=1+A$$
39	1 13 14 4 15 31 38	efsep	$$⊢A\in ℂ\to {\mathrm{e}}^A=1+A+\sum _{k\in {\mathbb{Z}}_{\ge 2}}F\left(k\right)$$
40		fac2	$$⊢2!=2$$
41	40	oveq2i	$$⊢\frac{A^2}{2!}=\frac{A^2}{2}$$
42	41	oveq2i	$$⊢1+A+\left(\frac{A^2}{2!}\right)=1+A+\left(\frac{A^2}{2}\right)$$
43	42	a1i	$$⊢A\in ℂ\to 1+A+\left(\frac{A^2}{2!}\right)=1+A+\left(\frac{A^2}{2}\right)$$
44	1 11 12 4 7 39 43	efsep	$$⊢A\in ℂ\to {\mathrm{e}}^A=\left(1+A\right)+\left(\frac{A^2}{2}\right)+\sum _{k\in {\mathbb{Z}}_{\ge 3}}F\left(k\right)$$
45		fac3	$$⊢3!=6$$
46	45	oveq2i	$$⊢\frac{A^3}{3!}=\frac{A^3}{6}$$
47	46	oveq2i	$$⊢\left(1+A\right)+\left(\frac{A^2}{2}\right)+\left(\frac{A^3}{3!}\right)=\left(1+A\right)+\left(\frac{A^2}{2}\right)+\left(\frac{A^3}{6}\right)$$
48	47	a1i	$$⊢A\in ℂ\to \left(1+A\right)+\left(\frac{A^2}{2}\right)+\left(\frac{A^3}{3!}\right)=\left(1+A\right)+\left(\frac{A^2}{2}\right)+\left(\frac{A^3}{6}\right)$$
49	1 2 3 4 10 44 48	efsep	$$⊢A\in ℂ\to {\mathrm{e}}^A=\left(1+A+\left(\frac{A^2}{2}\right)\right)+\left(\frac{A^3}{6}\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$