Theorem sinhneg

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

	Ref	Expression
Assertion	sinhneg	|- ( A e. CC -> ( sinh ` -u A ) = -u ( sinh ` A ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2	1	jctl	|- ( A e. CC -> ( _i e. CC /\ A e. CC ) )
3		mulcl	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4		sincl	|- ( ( _i x. A ) e. CC -> ( sin ` ( _i x. A ) ) e. CC )
5	2 3 4	3syl	|- ( A e. CC -> ( sin ` ( _i x. A ) ) e. CC )
6	1	a1i	|- ( A e. CC -> _i e. CC )
7		ine0	|- _i =/= 0
8	7	a1i	|- ( A e. CC -> _i =/= 0 )
9	5 6 8	divnegd	|- ( A e. CC -> -u ( ( sin ` ( _i x. A ) ) / _i ) = ( -u ( sin ` ( _i x. A ) ) / _i ) )
10		sinhval-named	|- ( A e. CC -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
11	10	negeqd	|- ( A e. CC -> -u ( sinh ` A ) = -u ( ( sin ` ( _i x. A ) ) / _i ) )
12		negcl	|- ( A e. CC -> -u A e. CC )
13		sinhval-named	|- ( -u A e. CC -> ( sinh ` -u A ) = ( ( sin ` ( _i x. -u A ) ) / _i ) )
14	12 13	syl	|- ( A e. CC -> ( sinh ` -u A ) = ( ( sin ` ( _i x. -u A ) ) / _i ) )
15		mulneg2	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
16	2 15	syl	|- ( A e. CC -> ( _i x. -u A ) = -u ( _i x. A ) )
17	16	eqcomd	|- ( A e. CC -> -u ( _i x. A ) = ( _i x. -u A ) )
18	17	fveq2d	|- ( A e. CC -> ( sin ` -u ( _i x. A ) ) = ( sin ` ( _i x. -u A ) ) )
19	18	oveq1d	|- ( A e. CC -> ( ( sin ` -u ( _i x. A ) ) / _i ) = ( ( sin ` ( _i x. -u A ) ) / _i ) )
20		sinneg	|- ( ( _i x. A ) e. CC -> ( sin ` -u ( _i x. A ) ) = -u ( sin ` ( _i x. A ) ) )
21	2 3 20	3syl	|- ( A e. CC -> ( sin ` -u ( _i x. A ) ) = -u ( sin ` ( _i x. A ) ) )
22	21	oveq1d	|- ( A e. CC -> ( ( sin ` -u ( _i x. A ) ) / _i ) = ( -u ( sin ` ( _i x. A ) ) / _i ) )
23	14 19 22	3eqtr2d	|- ( A e. CC -> ( sinh ` -u A ) = ( -u ( sin ` ( _i x. A ) ) / _i ) )
24	9 11 23	3eqtr4rd	|- ( A e. CC -> ( sinh ` -u A ) = -u ( sinh ` A ) )