Theorem efi4p

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, 30-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		efi4p.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\mathrm{i}A}^n}{n!}\right)$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
4	2 3	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
5	1	ef4p	$$⊢\mathrm{i}A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\left(1+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^2}{2}\right)\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$
6	4 5	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\left(1+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^2}{2}\right)\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$
7		ax-1cn	$$⊢1\in ℂ$$
8		addcl	$$⊢\left(1\in ℂ\wedge \mathrm{i}A\in ℂ\right)\to 1+\mathrm{i}A\in ℂ$$
9	7 4 8	sylancr	$$⊢A\in ℂ\to 1+\mathrm{i}A\in ℂ$$
10	4	sqcld	$$⊢A\in ℂ\to {\mathrm{i}A}^2\in ℂ$$
11	10	halfcld	$$⊢A\in ℂ\to \frac{{\mathrm{i}A}^2}{2}\in ℂ$$
12		3nn0	$$⊢3\in {\mathbb{N}}_0$$
13		expcl	$$⊢\left(\mathrm{i}A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\mathrm{i}A}^3\in ℂ$$
14	4 12 13	sylancl	$$⊢A\in ℂ\to {\mathrm{i}A}^3\in ℂ$$
15		6cn	$$⊢6\in ℂ$$
16		6re	$$⊢6\in ℝ$$
17		6pos	$$⊢0<6$$
18	16 17	gt0ne0ii	$$⊢6\ne 0$$
19		divcl	$$⊢\left({\mathrm{i}A}^3\in ℂ\wedge 6\in ℂ\wedge 6\ne 0\right)\to \frac{{\mathrm{i}A}^3}{6}\in ℂ$$
20	15 18 19	mp3an23	$$⊢{\mathrm{i}A}^3\in ℂ\to \frac{{\mathrm{i}A}^3}{6}\in ℂ$$
21	14 20	syl	$$⊢A\in ℂ\to \frac{{\mathrm{i}A}^3}{6}\in ℂ$$
22	9 11 21	addassd	$$⊢A\in ℂ\to \left(1+\mathrm{i}A\right)+\left(\frac{{\mathrm{i}A}^2}{2}\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)=1+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^2}{2}\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)$$
23	7	a1i	$$⊢A\in ℂ\to 1\in ℂ$$
24	23 4 11 21	add4d	$$⊢A\in ℂ\to 1+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^2}{2}\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)=1+\left(\frac{{\mathrm{i}A}^2}{2}\right)+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^3}{6}\right)$$
25		2nn0	$$⊢2\in {\mathbb{N}}_0$$
26		mulexp	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
27	2 25 26	mp3an13	$$⊢A\in ℂ\to {\mathrm{i}A}^2={\mathrm{i}}^2{A}^2$$
28		i2	$$⊢{\mathrm{i}}^2=-1$$
29	28	oveq1i	$$⊢{\mathrm{i}}^2{A}^2=-1A^2$$
30	29	a1i	$$⊢A\in ℂ\to {\mathrm{i}}^2{A}^2=-1A^2$$
31		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
32	31	mulm1d	$$⊢A\in ℂ\to -1A^2=-A^2$$
33	27 30 32	3eqtrd	$$⊢A\in ℂ\to {\mathrm{i}A}^2=-A^2$$
34	33	oveq1d	$$⊢A\in ℂ\to \frac{{\mathrm{i}A}^2}{2}=\frac{-A^2}{2}$$
35		2cn	$$⊢2\in ℂ$$
36		2ne0	$$⊢2\ne 0$$
37		divneg	$$⊢\left(A^2\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to -\frac{A^2}{2}=\frac{-A^2}{2}$$
38	35 36 37	mp3an23	$$⊢A^2\in ℂ\to -\frac{A^2}{2}=\frac{-A^2}{2}$$
39	31 38	syl	$$⊢A\in ℂ\to -\frac{A^2}{2}=\frac{-A^2}{2}$$
40	34 39	eqtr4d	$$⊢A\in ℂ\to \frac{{\mathrm{i}A}^2}{2}=-\frac{A^2}{2}$$
41	40	oveq2d	$$⊢A\in ℂ\to 1+\left(\frac{{\mathrm{i}A}^2}{2}\right)=1+\left(-\frac{A^2}{2}\right)$$
42	31	halfcld	$$⊢A\in ℂ\to \frac{A^2}{2}\in ℂ$$
43		negsub	$$⊢\left(1\in ℂ\wedge \frac{A^2}{2}\in ℂ\right)\to 1+\left(-\frac{A^2}{2}\right)=1-\left(\frac{A^2}{2}\right)$$
44	7 42 43	sylancr	$$⊢A\in ℂ\to 1+\left(-\frac{A^2}{2}\right)=1-\left(\frac{A^2}{2}\right)$$
45	41 44	eqtrd	$$⊢A\in ℂ\to 1+\left(\frac{{\mathrm{i}A}^2}{2}\right)=1-\left(\frac{A^2}{2}\right)$$
46		mulexp	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\mathrm{i}A}^3={\mathrm{i}}^3{A}^3$$
47	2 12 46	mp3an13	$$⊢A\in ℂ\to {\mathrm{i}A}^3={\mathrm{i}}^3{A}^3$$
48		i3	$$⊢{\mathrm{i}}^3=-\mathrm{i}$$
49	48	oveq1i	$$⊢{\mathrm{i}}^3{A}^3=\left(-\mathrm{i}\right)A^3$$
50	47 49	syl6eq	$$⊢A\in ℂ\to {\mathrm{i}A}^3=\left(-\mathrm{i}\right)A^3$$
51	50	oveq1d	$$⊢A\in ℂ\to \frac{{\mathrm{i}A}^3}{6}=\frac{\left(-\mathrm{i}\right)A^3}{6}$$
52		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
53	12 52	mpan2	$$⊢A\in ℂ\to A^3\in ℂ$$
54		negicn	$$⊢-\mathrm{i}\in ℂ$$
55	15 18	pm3.2i	$$⊢\left(6\in ℂ\wedge 6\ne 0\right)$$
56		divass	$$⊢\left(-\mathrm{i}\in ℂ\wedge A^3\in ℂ\wedge \left(6\in ℂ\wedge 6\ne 0\right)\right)\to \frac{\left(-\mathrm{i}\right)A^3}{6}=\left(-\mathrm{i}\right)\left(\frac{A^3}{6}\right)$$
57	54 55 56	mp3an13	$$⊢A^3\in ℂ\to \frac{\left(-\mathrm{i}\right)A^3}{6}=\left(-\mathrm{i}\right)\left(\frac{A^3}{6}\right)$$
58	53 57	syl	$$⊢A\in ℂ\to \frac{\left(-\mathrm{i}\right)A^3}{6}=\left(-\mathrm{i}\right)\left(\frac{A^3}{6}\right)$$
59		divcl	$$⊢\left(A^3\in ℂ\wedge 6\in ℂ\wedge 6\ne 0\right)\to \frac{A^3}{6}\in ℂ$$
60	15 18 59	mp3an23	$$⊢A^3\in ℂ\to \frac{A^3}{6}\in ℂ$$
61	53 60	syl	$$⊢A\in ℂ\to \frac{A^3}{6}\in ℂ$$
62		mulneg12	$$⊢\left(\mathrm{i}\in ℂ\wedge \frac{A^3}{6}\in ℂ\right)\to \left(-\mathrm{i}\right)\left(\frac{A^3}{6}\right)=\mathrm{i}\left(-\frac{A^3}{6}\right)$$
63	2 61 62	sylancr	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)\left(\frac{A^3}{6}\right)=\mathrm{i}\left(-\frac{A^3}{6}\right)$$
64	51 58 63	3eqtrd	$$⊢A\in ℂ\to \frac{{\mathrm{i}A}^3}{6}=\mathrm{i}\left(-\frac{A^3}{6}\right)$$
65	64	oveq2d	$$⊢A\in ℂ\to \mathrm{i}A+\left(\frac{{\mathrm{i}A}^3}{6}\right)=\mathrm{i}A+\mathrm{i}\left(-\frac{A^3}{6}\right)$$
66	61	negcld	$$⊢A\in ℂ\to -\frac{A^3}{6}\in ℂ$$
67		adddi	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\wedge -\frac{A^3}{6}\in ℂ\right)\to \mathrm{i}\left(A+\left(-\frac{A^3}{6}\right)\right)=\mathrm{i}A+\mathrm{i}\left(-\frac{A^3}{6}\right)$$
68	2 67	mp3an1	$$⊢\left(A\in ℂ\wedge -\frac{A^3}{6}\in ℂ\right)\to \mathrm{i}\left(A+\left(-\frac{A^3}{6}\right)\right)=\mathrm{i}A+\mathrm{i}\left(-\frac{A^3}{6}\right)$$
69	66 68	mpdan	$$⊢A\in ℂ\to \mathrm{i}\left(A+\left(-\frac{A^3}{6}\right)\right)=\mathrm{i}A+\mathrm{i}\left(-\frac{A^3}{6}\right)$$
70		negsub	$$⊢\left(A\in ℂ\wedge \frac{A^3}{6}\in ℂ\right)\to A+\left(-\frac{A^3}{6}\right)=A-\left(\frac{A^3}{6}\right)$$
71	61 70	mpdan	$$⊢A\in ℂ\to A+\left(-\frac{A^3}{6}\right)=A-\left(\frac{A^3}{6}\right)$$
72	71	oveq2d	$$⊢A\in ℂ\to \mathrm{i}\left(A+\left(-\frac{A^3}{6}\right)\right)=\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)$$
73	65 69 72	3eqtr2d	$$⊢A\in ℂ\to \mathrm{i}A+\left(\frac{{\mathrm{i}A}^3}{6}\right)=\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)$$
74	45 73	oveq12d	$$⊢A\in ℂ\to 1+\left(\frac{{\mathrm{i}A}^2}{2}\right)+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^3}{6}\right)=1-\left(\frac{A^2}{2}\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)$$
75	22 24 74	3eqtrd	$$⊢A\in ℂ\to \left(1+\mathrm{i}A\right)+\left(\frac{{\mathrm{i}A}^2}{2}\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)=1-\left(\frac{A^2}{2}\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)$$
76	75	oveq1d	$$⊢A\in ℂ\to \left(1+\mathrm{i}A+\left(\frac{{\mathrm{i}A}^2}{2}\right)\right)+\left(\frac{{\mathrm{i}A}^3}{6}\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)=\left(1-\left(\frac{A^2}{2}\right)\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$
77	6 76	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\left(1-\left(\frac{A^2}{2}\right)\right)+\mathrm{i}\left(A-\left(\frac{A^3}{6}\right)\right)+\sum _{k\in {\mathbb{Z}}_{\ge 4}}F\left(k\right)$$