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 sin i A i = e A e A 2

Proof

Step Hyp Ref Expression
1 ixi i i = 1
2 1 oveq1i i i A = -1 A
3 ax-icn i
4 mulass i i A i i A = i i A
5 3 3 4 mp3an12 A i i A = i i A
6 mulm1 A -1 A = A
7 2 5 6 3eqtr3a A i i A = A
8 7 fveq2d A e i i A = e A
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 A = 1 A
15 negicn i
16 mulass i i A i i A = i i A
17 15 3 16 mp3an12 A i i A = i i A
18 mulid2 A 1 A = A
19 14 17 18 3eqtr3a A i i A = A
20 19 fveq2d A e i i A = e A
21 8 20 oveq12d A e i i A e i i A = e A e A
22 21 oveq1d A e i i A e i i A 2 i = e A e A 2 i
23 mulcl i A i A
24 3 23 mpan A i A
25 sinval i A sin i A = e i i A e i i A 2 i
26 24 25 syl A sin i A = e i i A e i i A 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 e A e A 2 = i e A e A 2
32 ine0 i 0
33 3 32 reccli 1 i
34 efcl A e A
35 negcl A A
36 efcl A e A
37 35 36 syl A e A
38 34 37 subcld A e A e A
39 38 halfcld A e A e A 2
40 mulneg12 1 i e A e A 2 1 i e A e A 2 = 1 i e A e A 2
41 33 39 40 sylancr A 1 i e A e A 2 = 1 i e A e A 2
42 2cnd A 2
43 2ne0 2 0
44 43 a1i A 2 0
45 38 42 44 divnegd A e A e A 2 = e A e A 2
46 34 37 negsubdi2d A e A e A = e A e A
47 46 oveq1d A e A e A 2 = e A e A 2
48 45 47 eqtrd A e A e A 2 = e A e A 2
49 48 oveq2d A 1 i e A e A 2 = 1 i e A e A 2
50 37 34 subcld A e A e A
51 50 halfcld A e A e A 2
52 3 a1i A i
53 32 a1i A i 0
54 51 52 53 divrec2d A e A e A 2 i = 1 i e A e A 2
55 50 42 52 44 53 divdiv1d A e A e A 2 i = e A e A 2 i
56 49 54 55 3eqtr2d A 1 i e A e A 2 = e A e A 2 i
57 41 56 eqtrd A 1 i e A e A 2 = e A e A 2 i
58 31 57 eqtr3id A i e A e A 2 = e A e A 2 i
59 22 26 58 3eqtr4d A sin i A = i e A e A 2
60 59 oveq1d A sin i A i = i e A e A 2 i
61 39 52 53 divcan3d A i e A e A 2 i = e A e A 2
62 60 61 eqtrd A sin i A i = e A e A 2