Theorem efival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005)

	Ref	Expression
Assertion	efival	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\cos A+\mathrm{i}\sin A$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
3	1 2	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
4		efcl	$$⊢\mathrm{i}A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}\in ℂ$$
5	3 4	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}\in ℂ$$
6		negicn	$$⊢-\mathrm{i}\in ℂ$$
7		mulcl	$$⊢\left(-\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left(-\mathrm{i}\right)A\in ℂ$$
8	6 7	mpan	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)A\in ℂ$$
9		efcl	$$⊢\left(-\mathrm{i}\right)A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ$$
10	8 9	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ$$
11	5 10	addcld	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ$$
12	5 10	subcld	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ$$
13		2cn	$$⊢2\in ℂ$$
14		2ne0	$$⊢2\ne 0$$
15	13 14	pm3.2i	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
16		divdir	$$⊢\left({\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\wedge {\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)}{2}=\left(\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)+\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)$$
17	15 16	mp3an3	$$⊢\left({\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\wedge {\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\right)\to \frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)}{2}=\left(\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)+\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)$$
18	11 12 17	syl2anc	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)}{2}=\left(\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)+\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)$$
19	10 5	pncan3d	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)A}+{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}={\mathrm{e}}^{\mathrm{i}A}$$
20	19	oveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)={\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\mathrm{i}A}$$
21	5 10 12	addassd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)={\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)$$
22	5	2timesd	$$⊢A\in ℂ\to 2{\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\mathrm{i}A}$$
23	20 21 22	3eqtr4d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)=2{\mathrm{e}}^{\mathrm{i}A}$$
24	23	oveq1d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)}{2}=\frac{2{\mathrm{e}}^{\mathrm{i}A}}{2}$$
25		divcan3	$$⊢\left({\mathrm{e}}^{\mathrm{i}A}\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{2{\mathrm{e}}^{\mathrm{i}A}}{2}={\mathrm{e}}^{\mathrm{i}A}$$
26	13 14 25	mp3an23	$$⊢{\mathrm{e}}^{\mathrm{i}A}\in ℂ\to \frac{2{\mathrm{e}}^{\mathrm{i}A}}{2}={\mathrm{e}}^{\mathrm{i}A}$$
27	5 26	syl	$$⊢A\in ℂ\to \frac{2{\mathrm{e}}^{\mathrm{i}A}}{2}={\mathrm{e}}^{\mathrm{i}A}$$
28	24 27	eqtr2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}+\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)}{2}$$
29		cosval	$$⊢A\in ℂ\to \cos A=\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}$$
30		2mulicn	$$⊢2\mathrm{i}\in ℂ$$
31		2muline0	$$⊢2\mathrm{i}\ne 0$$
32	30 31	pm3.2i	$$⊢\left(2\mathrm{i}\in ℂ\wedge 2\mathrm{i}\ne 0\right)$$
33		div12	$$⊢\left(\mathrm{i}\in ℂ\wedge {\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\wedge \left(2\mathrm{i}\in ℂ\wedge 2\mathrm{i}\ne 0\right)\right)\to \mathrm{i}\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}\right)=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{\mathrm{i}}{2\mathrm{i}}\right)$$
34	1 32 33	mp3an13	$$⊢{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\to \mathrm{i}\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}\right)=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{\mathrm{i}}{2\mathrm{i}}\right)$$
35	12 34	syl	$$⊢A\in ℂ\to \mathrm{i}\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}\right)=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{\mathrm{i}}{2\mathrm{i}}\right)$$
36		sinval	$$⊢A\in ℂ\to \sin A=\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}$$
37	36	oveq2d	$$⊢A\in ℂ\to \mathrm{i}\sin A=\mathrm{i}\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2\mathrm{i}}\right)$$
38		divrec	$$⊢\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{1}{2}\right)$$
39	13 14 38	mp3an23	$$⊢{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{1}{2}\right)$$
40	12 39	syl	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{1}{2}\right)$$
41	1	mulid2i	$$⊢1\mathrm{i}=\mathrm{i}$$
42	41	oveq1i	$$⊢\frac{1\mathrm{i}}{2\mathrm{i}}=\frac{\mathrm{i}}{2\mathrm{i}}$$
43		ine0	$$⊢\mathrm{i}\ne 0$$
44	1 43	dividi	$$⊢\frac{\mathrm{i}}{\mathrm{i}}=1$$
45	44	oveq2i	$$⊢\left(\frac{1}{2}\right)\left(\frac{\mathrm{i}}{\mathrm{i}}\right)=\left(\frac{1}{2}\right)\cdot 1$$
46		ax-1cn	$$⊢1\in ℂ$$
47	46 13 1 1 14 43	divmuldivi	$$⊢\left(\frac{1}{2}\right)\left(\frac{\mathrm{i}}{\mathrm{i}}\right)=\frac{1\mathrm{i}}{2\mathrm{i}}$$
48	45 47	eqtr3i	$$⊢\left(\frac{1}{2}\right)\cdot 1=\frac{1\mathrm{i}}{2\mathrm{i}}$$
49		halfcn	$$⊢\frac{1}{2}\in ℂ$$
50	49	mulid1i	$$⊢\left(\frac{1}{2}\right)\cdot 1=\frac{1}{2}$$
51	48 50	eqtr3i	$$⊢\frac{1\mathrm{i}}{2\mathrm{i}}=\frac{1}{2}$$
52	42 51	eqtr3i	$$⊢\frac{\mathrm{i}}{2\mathrm{i}}=\frac{1}{2}$$
53	52	oveq2i	$$⊢\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{\mathrm{i}}{2\mathrm{i}}\right)=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{1}{2}\right)$$
54	40 53	eqtr4di	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}=\left({\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}\right)\left(\frac{\mathrm{i}}{2\mathrm{i}}\right)$$
55	35 37 54	3eqtr4d	$$⊢A\in ℂ\to \mathrm{i}\sin A=\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}$$
56	29 55	oveq12d	$$⊢A\in ℂ\to \cos A+\mathrm{i}\sin A=\left(\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)+\left(\frac{{\mathrm{e}}^{\mathrm{i}A}-{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\right)$$
57	18 28 56	3eqtr4d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\cos A+\mathrm{i}\sin A$$