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 ( 𝐴 ∈ ℂ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
4 cosval ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ ( i · ( i · 𝐴 ) ) ) + ( exp ‘ ( - i · ( i · 𝐴 ) ) ) ) / 2 ) )
5 3 4 syl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ ( i · ( i · 𝐴 ) ) ) + ( exp ‘ ( - i · ( i · 𝐴 ) ) ) ) / 2 ) )
6 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
7 efcl ⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ - 𝐴 ) ∈ ℂ )
8 6 7 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - 𝐴 ) ∈ ℂ )
9 efcl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
10 ixi ⊢ ( i · i ) = - 1
11 10 oveq1i ⊢ ( ( i · i ) · 𝐴 ) = ( - 1 · 𝐴 )
12 mulass ⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i · i ) · 𝐴 ) = ( i · ( i · 𝐴 ) ) )
13 1 1 12 mp3an12 ⊢ ( 𝐴 ∈ ℂ → ( ( i · i ) · 𝐴 ) = ( i · ( i · 𝐴 ) ) )
14 mulm1 ⊢ ( 𝐴 ∈ ℂ → ( - 1 · 𝐴 ) = - 𝐴 )
15 11 13 14 3eqtr3a ⊢ ( 𝐴 ∈ ℂ → ( i · ( i · 𝐴 ) ) = - 𝐴 )
16 15 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( i · 𝐴 ) ) ) = ( exp ‘ - 𝐴 ) )
17 1 1 mulneg1i ⊢ ( - i · i ) = - ( i · i )
18 10 negeqi ⊢ - ( i · i ) = - - 1
19 negneg1e1 ⊢ - - 1 = 1
20 17 18 19 3eqtri ⊢ ( - i · i ) = 1
21 20 oveq1i ⊢ ( ( - i · i ) · 𝐴 ) = ( 1 · 𝐴 )
22 negicn ⊢ - i ∈ ℂ
23 mulass ⊢ ( ( - i ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( - i · i ) · 𝐴 ) = ( - i · ( i · 𝐴 ) ) )
24 22 1 23 mp3an12 ⊢ ( 𝐴 ∈ ℂ → ( ( - i · i ) · 𝐴 ) = ( - i · ( i · 𝐴 ) ) )
25 mullid ⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
26 21 24 25 3eqtr3a ⊢ ( 𝐴 ∈ ℂ → ( - i · ( i · 𝐴 ) ) = 𝐴 )
27 26 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · ( i · 𝐴 ) ) ) = ( exp ‘ 𝐴 ) )
28 16 27 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( i · 𝐴 ) ) ) + ( exp ‘ ( - i · ( i · 𝐴 ) ) ) ) = ( ( exp ‘ - 𝐴 ) + ( exp ‘ 𝐴 ) ) )
29 8 9 28 comraddd ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · ( i · 𝐴 ) ) ) + ( exp ‘ ( - i · ( i · 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) )
30 29 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · ( i · 𝐴 ) ) ) + ( exp ‘ ( - i · ( i · 𝐴 ) ) ) ) / 2 ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )
31 5 30 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )