Theorem tanhneg

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

	Ref	Expression
Assertion	tanhneg	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ - 𝐴 ) = - ( tanh ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sinhcl	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( sinh ‘ 𝐴 ) ∈ ℂ )
3		coshcl	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ∈ ℂ )
5		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ≠ 0 )
6	2 4 5	divnegd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → - ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) = ( - ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
7		tanhval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
8	7	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → - ( tanh ‘ 𝐴 ) = - ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
9		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
10		coshneg	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cosh ‘ 𝐴 ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ - 𝐴 ) = ( cosh ‘ 𝐴 ) )
12	11 5	eqnetrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ - 𝐴 ) ≠ 0 )
13		tanhval	⊢ ( ( - 𝐴 ∈ ℂ ∧ ( cosh ‘ - 𝐴 ) ≠ 0 ) → ( tanh ‘ - 𝐴 ) = ( ( sinh ‘ - 𝐴 ) / ( cosh ‘ - 𝐴 ) ) )
14	9 12 13	syl2an2r	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ - 𝐴 ) = ( ( sinh ‘ - 𝐴 ) / ( cosh ‘ - 𝐴 ) ) )
15		sinhneg	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ - 𝐴 ) = - ( sinh ‘ 𝐴 ) )
16	15	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( sinh ‘ - 𝐴 ) = - ( sinh ‘ 𝐴 ) )
17	16 11	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( sinh ‘ - 𝐴 ) / ( cosh ‘ - 𝐴 ) ) = ( - ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
18	14 17	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ - 𝐴 ) = ( - ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
19	6 8 18	3eqtr4rd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ - 𝐴 ) = - ( tanh ‘ 𝐴 ) )