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 AsiniAi=eAeA2

Proof

Step Hyp Ref Expression
1 ixi ii=1
2 1 oveq1i iiA=-1A
3 ax-icn i
4 mulass iiAiiA=iiA
5 3 3 4 mp3an12 AiiA=iiA
6 mulm1 A-1A=A
7 2 5 6 3eqtr3a AiiA=A
8 7 fveq2d AeiiA=eA
9 3 3 mulneg1i ii=ii
10 1 negeqi ii=-1
11 negneg1e1 -1=1
12 10 11 eqtri ii=1
13 9 12 eqtri ii=1
14 13 oveq1i iiA=1A
15 negicn i
16 mulass iiAiiA=iiA
17 15 3 16 mp3an12 AiiA=iiA
18 mulid2 A1A=A
19 14 17 18 3eqtr3a AiiA=A
20 19 fveq2d AeiiA=eA
21 8 20 oveq12d AeiiAeiiA=eAeA
22 21 oveq1d AeiiAeiiA2i=eAeA2i
23 mulcl iAiA
24 3 23 mpan AiA
25 sinval iAsiniA=eiiAeiiA2i
26 24 25 syl AsiniA=eiiAeiiA2i
27 irec 1i=i
28 27 negeqi 1i=i
29 3 negnegi i=i
30 28 29 eqtri 1i=i
31 30 oveq1i 1ieAeA2=ieAeA2
32 ine0 i0
33 3 32 reccli 1i
34 efcl AeA
35 negcl AA
36 efcl AeA
37 35 36 syl AeA
38 34 37 subcld AeAeA
39 38 halfcld AeAeA2
40 mulneg12 1ieAeA21ieAeA2=1ieAeA2
41 33 39 40 sylancr A1ieAeA2=1ieAeA2
42 2cnd A2
43 2ne0 20
44 43 a1i A20
45 38 42 44 divnegd AeAeA2=eAeA2
46 34 37 negsubdi2d AeAeA=eAeA
47 46 oveq1d AeAeA2=eAeA2
48 45 47 eqtrd AeAeA2=eAeA2
49 48 oveq2d A1ieAeA2=1ieAeA2
50 37 34 subcld AeAeA
51 50 halfcld AeAeA2
52 3 a1i Ai
53 32 a1i Ai0
54 51 52 53 divrec2d AeAeA2i=1ieAeA2
55 50 42 52 44 53 divdiv1d AeAeA2i=eAeA2i
56 49 54 55 3eqtr2d A1ieAeA2=eAeA2i
57 41 56 eqtrd A1ieAeA2=eAeA2i
58 31 57 eqtr3id AieAeA2=eAeA2i
59 22 26 58 3eqtr4d AsiniA=ieAeA2
60 59 oveq1d AsiniAi=ieAeA2i
61 39 52 53 divcan3d AieAeA2i=eAeA2
62 60 61 eqtrd AsiniAi=eAeA2