Theorem sinhf

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

	Ref	Expression
Assertion	sinhf	|- sinh : CC --> CC

Proof

Step	Hyp	Ref	Expression
1		df-sinh	|- sinh = ( x e. CC |-> ( ( sin ` ( _i x. x ) ) / _i ) )
2		ax-icn	|- _i e. CC
3	2	a1i	|- ( x e. CC -> _i e. CC )
4		id	|- ( x e. CC -> x e. CC )
5	3 4	mulcld	|- ( x e. CC -> ( _i x. x ) e. CC )
6	5	sincld	|- ( x e. CC -> ( sin ` ( _i x. x ) ) e. CC )
7		ine0	|- _i =/= 0
8	7	a1i	|- ( x e. CC -> _i =/= 0 )
9	6 3 8	divcld	|- ( x e. CC -> ( ( sin ` ( _i x. x ) ) / _i ) e. CC )
10	1 9	fmpti	|- sinh : CC --> CC