Theorem tanhcl

Description: The closure of the tanh function with complex argument. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Assertion	tanhcl	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		coshcl	$$⊢A\in ℂ\to \cosh \left(A\right)\in ℂ$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\in ℂ$$
3		simpr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\ne 0$$
4	2 3	eldifsnd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
5		coshf	$$⊢\cosh :ℂ⟶ℂ$$
6		ffn	$$⊢\cosh :ℂ⟶ℂ\to \cosh Fnℂ$$
7		elpreima	$$⊢\cosh Fnℂ\to \left(A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
8	5 6 7	mp2b	$$⊢A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
9		tanhf	$$⊢\tanh :{\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟶ℂ$$
10	9	ffvelcdmi	$$⊢A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \tanh \left(A\right)\in ℂ$$
11	8 10	sylbir	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \tanh \left(A\right)\in ℂ$$
12	4 11	syldan	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(A\right)\in ℂ$$