Theorem sinh0

Description: Value of the sinh function at 0. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Assertion	sinh0	⊢ ( sinh ‘ 0 ) = 0

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		sinhval-named	⊢ ( 0 ∈ ℂ → ( sinh ‘ 0 ) = ( ( sin ‘ ( i · 0 ) ) / i ) )
3	1 2	ax-mp	⊢ ( sinh ‘ 0 ) = ( ( sin ‘ ( i · 0 ) ) / i )
4		it0e0	⊢ ( i · 0 ) = 0
5	4	fveq2i	⊢ ( sin ‘ ( i · 0 ) ) = ( sin ‘ 0 )
6		sin0	⊢ ( sin ‘ 0 ) = 0
7	5 6	eqtri	⊢ ( sin ‘ ( i · 0 ) ) = 0
8	7	oveq1i	⊢ ( ( sin ‘ ( i · 0 ) ) / i ) = ( 0 / i )
9		ax-icn	⊢ i ∈ ℂ
10		ine0	⊢ i ≠ 0
11	9 10	div0i	⊢ ( 0 / i ) = 0
12	3 8 11	3eqtri	⊢ ( sinh ‘ 0 ) = 0