Description: Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | sinhval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ixi | |
|
2 | 1 | oveq1i | |
3 | ax-icn | |
|
4 | mulass | |
|
5 | 3 3 4 | mp3an12 | |
6 | mulm1 | |
|
7 | 2 5 6 | 3eqtr3a | |
8 | 7 | fveq2d | |
9 | 3 3 | mulneg1i | |
10 | 1 | negeqi | |
11 | negneg1e1 | |
|
12 | 10 11 | eqtri | |
13 | 9 12 | eqtri | |
14 | 13 | oveq1i | |
15 | negicn | |
|
16 | mulass | |
|
17 | 15 3 16 | mp3an12 | |
18 | mulid2 | |
|
19 | 14 17 18 | 3eqtr3a | |
20 | 19 | fveq2d | |
21 | 8 20 | oveq12d | |
22 | 21 | oveq1d | |
23 | mulcl | |
|
24 | 3 23 | mpan | |
25 | sinval | |
|
26 | 24 25 | syl | |
27 | irec | |
|
28 | 27 | negeqi | |
29 | 3 | negnegi | |
30 | 28 29 | eqtri | |
31 | 30 | oveq1i | |
32 | ine0 | |
|
33 | 3 32 | reccli | |
34 | efcl | |
|
35 | negcl | |
|
36 | efcl | |
|
37 | 35 36 | syl | |
38 | 34 37 | subcld | |
39 | 38 | halfcld | |
40 | mulneg12 | |
|
41 | 33 39 40 | sylancr | |
42 | 2cnd | |
|
43 | 2ne0 | |
|
44 | 43 | a1i | |
45 | 38 42 44 | divnegd | |
46 | 34 37 | negsubdi2d | |
47 | 46 | oveq1d | |
48 | 45 47 | eqtrd | |
49 | 48 | oveq2d | |
50 | 37 34 | subcld | |
51 | 50 | halfcld | |
52 | 3 | a1i | |
53 | 32 | a1i | |
54 | 51 52 53 | divrec2d | |
55 | 50 42 52 44 53 | divdiv1d | |
56 | 49 54 55 | 3eqtr2d | |
57 | 41 56 | eqtrd | |
58 | 31 57 | eqtr3id | |
59 | 22 26 58 | 3eqtr4d | |
60 | 59 | oveq1d | |
61 | 39 52 53 | divcan3d | |
62 | 60 61 | eqtrd | |