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{e^{i A} + e^{(- i) A}}{2}$

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

Metamath Proof Explorer