Theorem coshf

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

	Ref	Expression
Assertion	coshf	|- cosh : CC --> CC

Proof

Step	Hyp	Ref	Expression
1		df-cosh	|- cosh = ( x e. CC |-> ( cos ` ( _i x. x ) ) )
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	coscld	|- ( x e. CC -> ( cos ` ( _i x. x ) ) e. CC )
7	1 6	fmpti	|- cosh : CC --> CC