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

Proof

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