Theorem sinhneg

Description: The sinh function is odd. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Assertion	sinhneg	$$⊢A\in ℂ\to \sinh \left(-A\right)=-\sinh \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2	1	jctl	$$⊢A\in ℂ\to \left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
4		sincl	$$⊢\mathrm{i}A\in ℂ\to \sin \mathrm{i}A\in ℂ$$
5	2 3 4	3syl	$$⊢A\in ℂ\to \sin \mathrm{i}A\in ℂ$$
6	1	a1i	$$⊢A\in ℂ\to \mathrm{i}\in ℂ$$
7		ine0	$$⊢\mathrm{i}\ne 0$$
8	7	a1i	$$⊢A\in ℂ\to \mathrm{i}\ne 0$$
9	5 6 8	divnegd	$$⊢A\in ℂ\to -\frac{\sin \mathrm{i}A}{\mathrm{i}}=\frac{-\sin \mathrm{i}A}{\mathrm{i}}$$
10		sinhval-named	$$⊢A\in ℂ\to \sinh \left(A\right)=\frac{\sin \mathrm{i}A}{\mathrm{i}}$$
11	10	negeqd	$$⊢A\in ℂ\to -\sinh \left(A\right)=-\frac{\sin \mathrm{i}A}{\mathrm{i}}$$
12		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
13		sinhval-named	$$⊢-A\in ℂ\to \sinh \left(-A\right)=\frac{\sin \mathrm{i}\left(-A\right)}{\mathrm{i}}$$
14	12 13	syl	$$⊢A\in ℂ\to \sinh \left(-A\right)=\frac{\sin \mathrm{i}\left(-A\right)}{\mathrm{i}}$$
15		mulneg2	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
16	2 15	syl	$$⊢A\in ℂ\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
17	16	eqcomd	$$⊢A\in ℂ\to -\mathrm{i}A=\mathrm{i}\left(-A\right)$$
18	17	fveq2d	$$⊢A\in ℂ\to \sin \left(-\mathrm{i}A\right)=\sin \mathrm{i}\left(-A\right)$$
19	18	oveq1d	$$⊢A\in ℂ\to \frac{\sin \left(-\mathrm{i}A\right)}{\mathrm{i}}=\frac{\sin \mathrm{i}\left(-A\right)}{\mathrm{i}}$$
20		sinneg	$$⊢\mathrm{i}A\in ℂ\to \sin \left(-\mathrm{i}A\right)=-\sin \mathrm{i}A$$
21	2 3 20	3syl	$$⊢A\in ℂ\to \sin \left(-\mathrm{i}A\right)=-\sin \mathrm{i}A$$
22	21	oveq1d	$$⊢A\in ℂ\to \frac{\sin \left(-\mathrm{i}A\right)}{\mathrm{i}}=\frac{-\sin \mathrm{i}A}{\mathrm{i}}$$
23	14 19 22	3eqtr2d	$$⊢A\in ℂ\to \sinh \left(-A\right)=\frac{-\sin \mathrm{i}A}{\mathrm{i}}$$
24	9 11 23	3eqtr4rd	$$⊢A\in ℂ\to \sinh \left(-A\right)=-\sinh \left(A\right)$$