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 e. CC -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
3 1 2 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
4 cosval 
 |-  ( ( _i x. A ) e. CC -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` ( _i x. ( _i x. A ) ) ) + ( exp ` ( -u _i x. ( _i x. A ) ) ) ) / 2 ) )
5 3 4 syl 
 |-  ( A e. CC -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` ( _i x. ( _i x. A ) ) ) + ( exp ` ( -u _i x. ( _i x. A ) ) ) ) / 2 ) )
6 negcl 
 |-  ( A e. CC -> -u A e. CC )
7 efcl 
 |-  ( -u A e. CC -> ( exp ` -u A ) e. CC )
8 6 7 syl 
 |-  ( A e. CC -> ( exp ` -u A ) e. CC )
9 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
10 ixi 
 |-  ( _i x. _i ) = -u 1
11 10 oveq1i 
 |-  ( ( _i x. _i ) x. A ) = ( -u 1 x. A )
12 mulass 
 |-  ( ( _i e. CC /\ _i e. CC /\ A e. CC ) -> ( ( _i x. _i ) x. A ) = ( _i x. ( _i x. A ) ) )
13 1 1 12 mp3an12 
 |-  ( A e. CC -> ( ( _i x. _i ) x. A ) = ( _i x. ( _i x. A ) ) )
14 mulm1 
 |-  ( A e. CC -> ( -u 1 x. A ) = -u A )
15 11 13 14 3eqtr3a 
 |-  ( A e. CC -> ( _i x. ( _i x. A ) ) = -u A )
16 15 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( _i x. A ) ) ) = ( exp ` -u A ) )
17 1 1 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
18 10 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
19 negneg1e1 
 |-  -u -u 1 = 1
20 17 18 19 3eqtri 
 |-  ( -u _i x. _i ) = 1
21 20 oveq1i 
 |-  ( ( -u _i x. _i ) x. A ) = ( 1 x. A )
22 negicn 
 |-  -u _i e. CC
23 mulass 
 |-  ( ( -u _i e. CC /\ _i e. CC /\ A e. CC ) -> ( ( -u _i x. _i ) x. A ) = ( -u _i x. ( _i x. A ) ) )
24 22 1 23 mp3an12 
 |-  ( A e. CC -> ( ( -u _i x. _i ) x. A ) = ( -u _i x. ( _i x. A ) ) )
25 mulid2 
 |-  ( A e. CC -> ( 1 x. A ) = A )
26 21 24 25 3eqtr3a 
 |-  ( A e. CC -> ( -u _i x. ( _i x. A ) ) = A )
27 26 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( _i x. A ) ) ) = ( exp ` A ) )
28 16 27 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( _i x. A ) ) ) + ( exp ` ( -u _i x. ( _i x. A ) ) ) ) = ( ( exp ` -u A ) + ( exp ` A ) ) )
29 8 9 28 comraddd 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( _i x. A ) ) ) + ( exp ` ( -u _i x. ( _i x. A ) ) ) ) = ( ( exp ` A ) + ( exp ` -u A ) ) )
30 29 oveq1d 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. ( _i x. A ) ) ) + ( exp ` ( -u _i x. ( _i x. A ) ) ) ) / 2 ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )
31 5 30 eqtrd 
 |-  ( A e. CC -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )