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 = ( 𝑥 ∈ ℂ ↦ ( cos ‘ ( i · 𝑥 ) ) )
2		ax-icn	⊢ i ∈ ℂ
3	2	a1i	⊢ ( 𝑥 ∈ ℂ → i ∈ ℂ )
4		id	⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
5	3 4	mulcld	⊢ ( 𝑥 ∈ ℂ → ( i · 𝑥 ) ∈ ℂ )
6	5	coscld	⊢ ( 𝑥 ∈ ℂ → ( cos ‘ ( i · 𝑥 ) ) ∈ ℂ )
7	1 6	fmpti	⊢ cosh : ℂ ⟶ ℂ