Theorem efmival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006)

	Ref	Expression
Assertion	efmival	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)A}=\cos A-\mathrm{i}\sin A$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		mulneg12	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left(-\mathrm{i}\right)A=\mathrm{i}\left(-A\right)$$
3	1 2	mpan	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)A=\mathrm{i}\left(-A\right)$$
4	3	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)A}={\mathrm{e}}^{\mathrm{i}\left(-A\right)}$$
5		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
6		efival	$$⊢-A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(-A\right)}=\cos \left(-A\right)+\mathrm{i}\sin \left(-A\right)$$
7	5 6	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(-A\right)}=\cos \left(-A\right)+\mathrm{i}\sin \left(-A\right)$$
8		cosneg	$$⊢A\in ℂ\to \cos \left(-A\right)=\cos A$$
9		sinneg	$$⊢A\in ℂ\to \sin \left(-A\right)=-\sin A$$
10	9	oveq2d	$$⊢A\in ℂ\to \mathrm{i}\sin \left(-A\right)=\mathrm{i}\left(-\sin A\right)$$
11		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
12		mulneg2	$$⊢\left(\mathrm{i}\in ℂ\wedge \sin A\in ℂ\right)\to \mathrm{i}\left(-\sin A\right)=-\mathrm{i}\sin A$$
13	1 11 12	sylancr	$$⊢A\in ℂ\to \mathrm{i}\left(-\sin A\right)=-\mathrm{i}\sin A$$
14	10 13	eqtrd	$$⊢A\in ℂ\to \mathrm{i}\sin \left(-A\right)=-\mathrm{i}\sin A$$
15	8 14	oveq12d	$$⊢A\in ℂ\to \cos \left(-A\right)+\mathrm{i}\sin \left(-A\right)=\cos A+\left(-\mathrm{i}\sin A\right)$$
16		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
17		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \sin A\in ℂ\right)\to \mathrm{i}\sin A\in ℂ$$
18	1 11 17	sylancr	$$⊢A\in ℂ\to \mathrm{i}\sin A\in ℂ$$
19	16 18	negsubd	$$⊢A\in ℂ\to \cos A+\left(-\mathrm{i}\sin A\right)=\cos A-\mathrm{i}\sin A$$
20	15 19	eqtrd	$$⊢A\in ℂ\to \cos \left(-A\right)+\mathrm{i}\sin \left(-A\right)=\cos A-\mathrm{i}\sin A$$
21	7 20	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(-A\right)}=\cos A-\mathrm{i}\sin A$$
22	4 21	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)A}=\cos A-\mathrm{i}\sin A$$