Theorem sinhval

Description: Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015)

	Ref	Expression
Assertion	sinhval	$$⊢A\in ℂ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}$$

Proof

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