Theorem tanhneg

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

	Ref	Expression
Assertion	tanhneg	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` -u A ) = -u ( tanh ` A ) )

Proof

Step	Hyp	Ref	Expression
1		sinhcl	|- ( A e. CC -> ( sinh ` A ) e. CC )
2	1	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( sinh ` A ) e. CC )
3		coshcl	|- ( A e. CC -> ( cosh ` A ) e. CC )
4	3	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) e. CC )
5		simpr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) =/= 0 )
6	2 4 5	divnegd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> -u ( ( sinh ` A ) / ( cosh ` A ) ) = ( -u ( sinh ` A ) / ( cosh ` A ) ) )
7		tanhval	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( sinh ` A ) / ( cosh ` A ) ) )
8	7	negeqd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> -u ( tanh ` A ) = -u ( ( sinh ` A ) / ( cosh ` A ) ) )
9		negcl	|- ( A e. CC -> -u A e. CC )
10		coshneg	|- ( A e. CC -> ( cosh ` -u A ) = ( cosh ` A ) )
11	10	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` -u A ) = ( cosh ` A ) )
12	11 5	eqnetrd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` -u A ) =/= 0 )
13		tanhval	|- ( ( -u A e. CC /\ ( cosh ` -u A ) =/= 0 ) -> ( tanh ` -u A ) = ( ( sinh ` -u A ) / ( cosh ` -u A ) ) )
14	9 12 13	syl2an2r	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` -u A ) = ( ( sinh ` -u A ) / ( cosh ` -u A ) ) )
15		sinhneg	|- ( A e. CC -> ( sinh ` -u A ) = -u ( sinh ` A ) )
16	15	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( sinh ` -u A ) = -u ( sinh ` A ) )
17	16 11	oveq12d	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( sinh ` -u A ) / ( cosh ` -u A ) ) = ( -u ( sinh ` A ) / ( cosh ` A ) ) )
18	14 17	eqtrd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` -u A ) = ( -u ( sinh ` A ) / ( cosh ` A ) ) )
19	6 8 18	3eqtr4rd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` -u A ) = -u ( tanh ` A ) )