# Metamath Proof Explorer

## 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 \mathrm{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 \mathrm{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 \mathrm{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}=-1{A}$
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 -1{A}=-{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}=1{A}$
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 mulid2 ${⊢}{A}\in ℂ\to 1{A}={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 \mathrm{cos}\mathrm{i}{A}=\frac{{\mathrm{e}}^{{A}}+{\mathrm{e}}^{-{A}}}{2}$