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 = ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ ( i · 𝑥 ) ) / i ) )
2		ax-icn	⊢ i ∈ ℂ
3	2	a1i	⊢ ( 𝑥 ∈ ℂ → i ∈ ℂ )
4		id	⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
5	3 4	mulcld	⊢ ( 𝑥 ∈ ℂ → ( i · 𝑥 ) ∈ ℂ )
6	5	sincld	⊢ ( 𝑥 ∈ ℂ → ( sin ‘ ( i · 𝑥 ) ) ∈ ℂ )
7		ine0	⊢ i ≠ 0
8	7	a1i	⊢ ( 𝑥 ∈ ℂ → i ≠ 0 )
9	6 3 8	divcld	⊢ ( 𝑥 ∈ ℂ → ( ( sin ‘ ( i · 𝑥 ) ) / i ) ∈ ℂ )
10	1 9	fmpti	⊢ sinh : ℂ ⟶ ℂ