Theorem sinhneg

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

	Ref	Expression
Assertion	sinhneg	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ - 𝐴 ) = - ( sinh ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2	1	jctl	⊢ ( 𝐴 ∈ ℂ → ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
3		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4		sincl	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ )
5	2 3 4	3syl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ )
6	1	a1i	⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
7		ine0	⊢ i ≠ 0
8	7	a1i	⊢ ( 𝐴 ∈ ℂ → i ≠ 0 )
9	5 6 8	divnegd	⊢ ( 𝐴 ∈ ℂ → - ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( - ( sin ‘ ( i · 𝐴 ) ) / i ) )
10		sinhval-named	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( ( sin ‘ ( i · 𝐴 ) ) / i ) )
11	10	negeqd	⊢ ( 𝐴 ∈ ℂ → - ( sinh ‘ 𝐴 ) = - ( ( sin ‘ ( i · 𝐴 ) ) / i ) )
12		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
13		sinhval-named	⊢ ( - 𝐴 ∈ ℂ → ( sinh ‘ - 𝐴 ) = ( ( sin ‘ ( i · - 𝐴 ) ) / i ) )
14	12 13	syl	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ - 𝐴 ) = ( ( sin ‘ ( i · - 𝐴 ) ) / i ) )
15		mulneg2	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
16	2 15	syl	⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
17	16	eqcomd	⊢ ( 𝐴 ∈ ℂ → - ( i · 𝐴 ) = ( i · - 𝐴 ) )
18	17	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - ( i · 𝐴 ) ) = ( sin ‘ ( i · - 𝐴 ) ) )
19	18	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ - ( i · 𝐴 ) ) / i ) = ( ( sin ‘ ( i · - 𝐴 ) ) / i ) )
20		sinneg	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( sin ‘ - ( i · 𝐴 ) ) = - ( sin ‘ ( i · 𝐴 ) ) )
21	2 3 20	3syl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - ( i · 𝐴 ) ) = - ( sin ‘ ( i · 𝐴 ) ) )
22	21	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ - ( i · 𝐴 ) ) / i ) = ( - ( sin ‘ ( i · 𝐴 ) ) / i ) )
23	14 19 22	3eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ - 𝐴 ) = ( - ( sin ‘ ( i · 𝐴 ) ) / i ) )
24	9 11 23	3eqtr4rd	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ - 𝐴 ) = - ( sinh ‘ 𝐴 ) )