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 ) )