Theorem tanhf

Description: Domain and codomain of the tanh function. (Contributed by Jon Pennant, 22-Oct-2026)

	Ref	Expression
Assertion	tanhf	$$⊢\tanh :{\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-tanh	$$⊢\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sinh \left(x\right)}{\cosh \left(x\right)}\right)$$
2		coshf	$$⊢\cosh :ℂ⟶ℂ$$
3		ffn	$$⊢\cosh :ℂ⟶ℂ\to \cosh Fnℂ$$
4		elpreima	$$⊢\cosh Fnℂ\to \left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(x\in ℂ\wedge \cosh \left(x\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
5	2 3 4	mp2b	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(x\in ℂ\wedge \cosh \left(x\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
6	5	simplbi	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to x\in ℂ$$
7		sinhcl	$$⊢x\in ℂ\to \sinh \left(x\right)\in ℂ$$
8	6 7	syl	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \sinh \left(x\right)\in ℂ$$
9		coshcl	$$⊢x\in ℂ\to \cosh \left(x\right)\in ℂ$$
10	6 9	syl	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cosh \left(x\right)\in ℂ$$
11	5	simprbi	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cosh \left(x\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
12	11	eldifsnbd	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cosh \left(x\right)\ne 0$$
13	8 10 12	divcld	$$⊢x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{\sinh \left(x\right)}{\cosh \left(x\right)}\in ℂ$$
14	1 13	fmpti	$$⊢\tanh :{\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟶ℂ$$