Theorem coshf

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

	Ref	Expression
Assertion	coshf	$$⊢\cosh :ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-cosh	$$⊢\cosh =\left(x\in ℂ⟼\cos \mathrm{i}x\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	coscld	$$⊢x\in ℂ\to \cos \mathrm{i}x\in ℂ$$
7	1 6	fmpti	$$⊢\cosh :ℂ⟶ℂ$$