Theorem sinh-conventional

Description: Conventional definition of sinh. Here we show that the sinh definition we're using has the same meaning as the conventional definition used in some other sources. We choose a slightly different definition of sinh because it has fewer operations, and thus is more convenient to manipulate using set.mm. (Contributed by David A. Wheeler, 10-May-2015)

	Ref	Expression
Assertion	sinh-conventional	$$⊢A\in ℂ\to \sinh \left(A\right)=\left(-\mathrm{i}\right)\sin \mathrm{i}A$$

Proof

Step	Hyp	Ref	Expression
1		sinhval-named	$$⊢A\in ℂ\to \sinh \left(A\right)=\frac{\sin \mathrm{i}A}{\mathrm{i}}$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
4	2 3	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
5	4	sincld	$$⊢A\in ℂ\to \sin \mathrm{i}A\in ℂ$$
6		ine0	$$⊢\mathrm{i}\ne 0$$
7		divrec2	$$⊢\left(\sin \mathrm{i}A\in ℂ\wedge \mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\left(\frac{1}{\mathrm{i}}\right)\sin \mathrm{i}A$$
8	2 6 7	mp3an23	$$⊢\sin \mathrm{i}A\in ℂ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\left(\frac{1}{\mathrm{i}}\right)\sin \mathrm{i}A$$
9	5 8	syl	$$⊢A\in ℂ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\left(\frac{1}{\mathrm{i}}\right)\sin \mathrm{i}A$$
10		irec	$$⊢\frac{1}{\mathrm{i}}=-\mathrm{i}$$
11	10	oveq1i	$$⊢\left(\frac{1}{\mathrm{i}}\right)\sin \mathrm{i}A=\left(-\mathrm{i}\right)\sin \mathrm{i}A$$
12	11	a1i	$$⊢A\in ℂ\to \left(\frac{1}{\mathrm{i}}\right)\sin \mathrm{i}A=\left(-\mathrm{i}\right)\sin \mathrm{i}A$$
13	1 9 12	3eqtrd	$$⊢A\in ℂ\to \sinh \left(A\right)=\left(-\mathrm{i}\right)\sin \mathrm{i}A$$