Theorem tanhneg

Description: The tanh function is odd. (Contributed by Jon Pennant, 22-Oct-2026)

	Ref	Expression
Assertion	tanhneg	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(-A\right)=-\tanh \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sinhcl	$$⊢A\in ℂ\to \sinh \left(A\right)\in ℂ$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \sinh \left(A\right)\in ℂ$$
3		coshcl	$$⊢A\in ℂ\to \cosh \left(A\right)\in ℂ$$
4	3	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\in ℂ$$
5		simpr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\ne 0$$
6	2 4 5	divnegd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to -\frac{\sinh \left(A\right)}{\cosh \left(A\right)}=\frac{-\sinh \left(A\right)}{\cosh \left(A\right)}$$
7		tanhval	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(A\right)=\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$
8	7	negeqd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to -\tanh \left(A\right)=-\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$
9		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
10		coshneg	$$⊢A\in ℂ\to \cosh \left(-A\right)=\cosh \left(A\right)$$
11	10	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(-A\right)=\cosh \left(A\right)$$
12	11 5	eqnetrd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(-A\right)\ne 0$$
13		tanhval	$$⊢\left(-A\in ℂ\wedge \cosh \left(-A\right)\ne 0\right)\to \tanh \left(-A\right)=\frac{\sinh \left(-A\right)}{\cosh \left(-A\right)}$$
14	9 12 13	syl2an2r	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(-A\right)=\frac{\sinh \left(-A\right)}{\cosh \left(-A\right)}$$
15		sinhneg	$$⊢A\in ℂ\to \sinh \left(-A\right)=-\sinh \left(A\right)$$
16	15	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \sinh \left(-A\right)=-\sinh \left(A\right)$$
17	16 11	oveq12d	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \frac{\sinh \left(-A\right)}{\cosh \left(-A\right)}=\frac{-\sinh \left(A\right)}{\cosh \left(A\right)}$$
18	14 17	eqtrd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(-A\right)=\frac{-\sinh \left(A\right)}{\cosh \left(A\right)}$$
19	6 8 18	3eqtr4rd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(-A\right)=-\tanh \left(A\right)$$