Theorem coshval

Description: Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015)

	Ref	Expression
Assertion	coshval	$$⊢A\in ℂ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$

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		cosval	$$⊢\mathrm{i}A\in ℂ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^{\mathrm{i}\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\mathrm{i}A}}{2}$$
5	3 4	syl	$$⊢A\in ℂ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^{\mathrm{i}\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\mathrm{i}A}}{2}$$
6		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
7		efcl	$$⊢-A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
8	6 7	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
9		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
10		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
11	10	oveq1i	$$⊢\mathrm{i}\mathrm{i}A=-1A$$
12		mulass	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}\mathrm{i}A=\mathrm{i}\mathrm{i}A$$
13	1 1 12	mp3an12	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}A=\mathrm{i}\mathrm{i}A$$
14		mulm1	$$⊢A\in ℂ\to -1A=-A$$
15	11 13 14	3eqtr3a	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}A=-A$$
16	15	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\mathrm{i}A}={\mathrm{e}}^{-A}$$
17	1 1	mulneg1i	$$⊢\left(-\mathrm{i}\right)\mathrm{i}=-\mathrm{i}\mathrm{i}$$
18	10	negeqi	$$⊢-\mathrm{i}\mathrm{i}=--1$$
19		negneg1e1	$$⊢--1=1$$
20	17 18 19	3eqtri	$$⊢\left(-\mathrm{i}\right)\mathrm{i}=1$$
21	20	oveq1i	$$⊢\left(-\mathrm{i}\right)\mathrm{i}A=1A$$
22		negicn	$$⊢-\mathrm{i}\in ℂ$$
23		mulass	$$⊢\left(-\mathrm{i}\in ℂ\wedge \mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left(-\mathrm{i}\right)\mathrm{i}A=\left(-\mathrm{i}\right)\mathrm{i}A$$
24	22 1 23	mp3an12	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)\mathrm{i}A=\left(-\mathrm{i}\right)\mathrm{i}A$$
25		mullid	$$⊢A\in ℂ\to 1A=A$$
26	21 24 25	3eqtr3a	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)\mathrm{i}A=A$$
27	26	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)\mathrm{i}A}={\mathrm{e}}^A$$
28	16 27	oveq12d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\mathrm{i}A}={\mathrm{e}}^{-A}+{\mathrm{e}}^A$$
29	8 9 28	comraddd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\mathrm{i}A}={\mathrm{e}}^A+{\mathrm{e}}^{-A}$$
30	29	oveq1d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}\mathrm{i}A}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\mathrm{i}A}}{2}=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$
31	5 30	eqtrd	$$⊢A\in ℂ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$