Theorem sinhf

Description: Domain and codomain of the sinh function. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Assertion	sinhf	$$⊢\sinh :ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-sinh	$$⊢\sinh =\left(x\in ℂ⟼\frac{\sin \mathrm{i}x}{\mathrm{i}}\right)$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3	2	a1i	$$⊢x\in ℂ\to \mathrm{i}\in ℂ$$
4		id	$$⊢x\in ℂ\to x\in ℂ$$
5	3 4	mulcld	$$⊢x\in ℂ\to \mathrm{i}x\in ℂ$$
6	5	sincld	$$⊢x\in ℂ\to \sin \mathrm{i}x\in ℂ$$
7		ine0	$$⊢\mathrm{i}\ne 0$$
8	7	a1i	$$⊢x\in ℂ\to \mathrm{i}\ne 0$$
9	6 3 8	divcld	$$⊢x\in ℂ\to \frac{\sin \mathrm{i}x}{\mathrm{i}}\in ℂ$$
10	1 9	fmpti	$$⊢\sinh :ℂ⟶ℂ$$