Theorem cosval

Description: Value of the cosine function. (Contributed by NM, 14-Mar-2005) (Revised by Mario Carneiro, 10-Nov-2013)

	Ref	Expression
Assertion	cosval	$$⊢A\in ℂ\to \cos A=\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
2	1	fveq2d	$$⊢x=A\to {\mathrm{e}}^{\mathrm{i}x}={\mathrm{e}}^{\mathrm{i}A}$$
3		oveq2	$$⊢x=A\to \left(-\mathrm{i}\right)x=\left(-\mathrm{i}\right)A$$
4	3	fveq2d	$$⊢x=A\to {\mathrm{e}}^{\left(-\mathrm{i}\right)x}={\mathrm{e}}^{\left(-\mathrm{i}\right)A}$$
5	2 4	oveq12d	$$⊢x=A\to {\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}={\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}$$
6	5	oveq1d	$$⊢x=A\to \frac{{\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2}=\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}$$
7		df-cos	$$⊢\cos =\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2}\right)$$
8		ovex	$$⊢\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢A\in ℂ\to \cos A=\frac{{\mathrm{e}}^{\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)A}}{2}$$