Theorem sinh0

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

	Ref	Expression
Assertion	sinh0	$$⊢\sinh \left(0\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		sinhval-named	$$⊢0\in ℂ\to \sinh \left(0\right)=\frac{\sin \mathrm{i}\cdot 0}{\mathrm{i}}$$
3	1 2	ax-mp	$$⊢\sinh \left(0\right)=\frac{\sin \mathrm{i}\cdot 0}{\mathrm{i}}$$
4		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
5	4	fveq2i	$$⊢\sin \mathrm{i}\cdot 0=\sin 0$$
6		sin0	$$⊢\sin 0=0$$
7	5 6	eqtri	$$⊢\sin \mathrm{i}\cdot 0=0$$
8	7	oveq1i	$$⊢\frac{\sin \mathrm{i}\cdot 0}{\mathrm{i}}=\frac{0}{\mathrm{i}}$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10		ine0	$$⊢\mathrm{i}\ne 0$$
11	9 10	div0i	$$⊢\frac{0}{\mathrm{i}}=0$$
12	3 8 11	3eqtri	$$⊢\sinh \left(0\right)=0$$