Metamath Proof Explorer

Theorem sinhval

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

Ref Expression
Assertion sinhval 
|- ( A e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 ixi 
 |-  ( _i x. _i ) = -u 1
2 1 oveq1i 
 |-  ( ( _i x. _i ) x. A ) = ( -u 1 x. A )
3 ax-icn 
 |-  _i e. CC
4 mulass 
 |-  ( ( _i e. CC /\ _i e. CC /\ A e. CC ) -> ( ( _i x. _i ) x. A ) = ( _i x. ( _i x. A ) ) )
5 3 3 4 mp3an12 
 |-  ( A e. CC -> ( ( _i x. _i ) x. A ) = ( _i x. ( _i x. A ) ) )
6 mulm1 
 |-  ( A e. CC -> ( -u 1 x. A ) = -u A )
7 2 5 6 3eqtr3a 
 |-  ( A e. CC -> ( _i x. ( _i x. A ) ) = -u A )
8 7 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( _i x. A ) ) ) = ( exp ` -u A ) )
9 3 3 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
10 1 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
11 negneg1e1 
 |-  -u -u 1 = 1
12 10 11 eqtri 
 |-  -u ( _i x. _i ) = 1
13 9 12 eqtri 
 |-  ( -u _i x. _i ) = 1
14 13 oveq1i 
 |-  ( ( -u _i x. _i ) x. A ) = ( 1 x. A )
15 negicn 
 |-  -u _i e. CC
16 mulass 
 |-  ( ( -u _i e. CC /\ _i e. CC /\ A e. CC ) -> ( ( -u _i x. _i ) x. A ) = ( -u _i x. ( _i x. A ) ) )
17 15 3 16 mp3an12 
 |-  ( A e. CC -> ( ( -u _i x. _i ) x. A ) = ( -u _i x. ( _i x. A ) ) )
18 mulid2 
 |-  ( A e. CC -> ( 1 x. A ) = A )
19 14 17 18 3eqtr3a 
 |-  ( A e. CC -> ( -u _i x. ( _i x. A ) ) = A )
20 19 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( _i x. A ) ) ) = ( exp ` A ) )
21 8 20 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( _i x. A ) ) ) - ( exp ` ( -u _i x. ( _i x. A ) ) ) ) = ( ( exp ` -u A ) - ( exp ` A ) ) )
22 21 oveq1d 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. ( _i x. A ) ) ) - ( exp ` ( -u _i x. ( _i x. A ) ) ) ) / ( 2 x. _i ) ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / ( 2 x. _i ) ) )
23 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
24 3 23 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
25 sinval 
 |-  ( ( _i x. A ) e. CC -> ( sin ` ( _i x. A ) ) = ( ( ( exp ` ( _i x. ( _i x. A ) ) ) - ( exp ` ( -u _i x. ( _i x. A ) ) ) ) / ( 2 x. _i ) ) )
26 24 25 syl 
 |-  ( A e. CC -> ( sin ` ( _i x. A ) ) = ( ( ( exp ` ( _i x. ( _i x. A ) ) ) - ( exp ` ( -u _i x. ( _i x. A ) ) ) ) / ( 2 x. _i ) ) )
27 irec 
 |-  ( 1 / _i ) = -u _i
28 27 negeqi 
 |-  -u ( 1 / _i ) = -u -u _i
29 3 negnegi 
 |-  -u -u _i = _i
30 28 29 eqtri 
 |-  -u ( 1 / _i ) = _i
31 30 oveq1i 
 |-  ( -u ( 1 / _i ) x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( _i x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
32 ine0 
 |-  _i =/= 0
33 3 32 reccli 
 |-  ( 1 / _i ) e. CC
34 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
35 negcl 
 |-  ( A e. CC -> -u A e. CC )
36 efcl 
 |-  ( -u A e. CC -> ( exp ` -u A ) e. CC )
37 35 36 syl 
 |-  ( A e. CC -> ( exp ` -u A ) e. CC )
38 34 37 subcld 
 |-  ( A e. CC -> ( ( exp ` A ) - ( exp ` -u A ) ) e. CC )
39 38 halfcld 
 |-  ( A e. CC -> ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) e. CC )
40 mulneg12 
 |-  ( ( ( 1 / _i ) e. CC /\ ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) e. CC ) -> ( -u ( 1 / _i ) x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( ( 1 / _i ) x. -u ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) )
41 33 39 40 sylancr 
 |-  ( A e. CC -> ( -u ( 1 / _i ) x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( ( 1 / _i ) x. -u ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) )
42 2cnd 
 |-  ( A e. CC -> 2 e. CC )
43 2ne0 
 |-  2 =/= 0
44 43 a1i 
 |-  ( A e. CC -> 2 =/= 0 )
45 38 42 44 divnegd 
 |-  ( A e. CC -> -u ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) = ( -u ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
46 34 37 negsubdi2d 
 |-  ( A e. CC -> -u ( ( exp ` A ) - ( exp ` -u A ) ) = ( ( exp ` -u A ) - ( exp ` A ) ) )
47 46 oveq1d 
 |-  ( A e. CC -> ( -u ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) )
48 45 47 eqtrd 
 |-  ( A e. CC -> -u ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) )
49 48 oveq2d 
 |-  ( A e. CC -> ( ( 1 / _i ) x. -u ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( ( 1 / _i ) x. ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) ) )
50 37 34 subcld 
 |-  ( A e. CC -> ( ( exp ` -u A ) - ( exp ` A ) ) e. CC )
51 50 halfcld 
 |-  ( A e. CC -> ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) e. CC )
52 3 a1i 
 |-  ( A e. CC -> _i e. CC )
53 32 a1i 
 |-  ( A e. CC -> _i =/= 0 )
54 51 52 53 divrec2d 
 |-  ( A e. CC -> ( ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) / _i ) = ( ( 1 / _i ) x. ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) ) )
55 50 42 52 44 53 divdiv1d 
 |-  ( A e. CC -> ( ( ( ( exp ` -u A ) - ( exp ` A ) ) / 2 ) / _i ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / ( 2 x. _i ) ) )
56 49 54 55 3eqtr2d 
 |-  ( A e. CC -> ( ( 1 / _i ) x. -u ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / ( 2 x. _i ) ) )
57 41 56 eqtrd 
 |-  ( A e. CC -> ( -u ( 1 / _i ) x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / ( 2 x. _i ) ) )
58 31 57 eqtr3id 
 |-  ( A e. CC -> ( _i x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) = ( ( ( exp ` -u A ) - ( exp ` A ) ) / ( 2 x. _i ) ) )
59 22 26 58 3eqtr4d 
 |-  ( A e. CC -> ( sin ` ( _i x. A ) ) = ( _i x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) )
60 59 oveq1d 
 |-  ( A e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( _i x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) / _i ) )
61 39 52 53 divcan3d 
 |-  ( A e. CC -> ( ( _i x. ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
62 60 61 eqtrd 
 |-  ( A e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )