Definition df-tanh

Description: Define the hyperbolic tangent function (tanh). We define it this way for cmpt , which requires the form ( x e. A |-> B ) . (Contributed by David A. Wheeler, 10-May-2015) (Revised by Jon Pennant, 22-Oct-2026)

	Ref	Expression
Assertion	df-tanh	$$⊢\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sinh \left(x\right)}{\cosh \left(x\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctanh	$$class\tanh$$
1		vx	$$setvarx$$
2		ccosh	$$class\cosh$$
3	2	ccnv	$$class{\cosh }^{-1}$$
4		cc	$$classℂ$$
5		cc0	$$class0$$
6	5	csn	$$class\left\{0\right\}$$
7	4 6	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
8	3 7	cima	$$class{\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
9		csinh	$$class\sinh$$
10	1	cv	$$setvarx$$
11	10 9	cfv	$$class\sinh \left(x\right)$$
12		cdiv	$$class÷$$
13	10 2	cfv	$$class\cosh \left(x\right)$$
14	11 13 12	co	$$class\left(\frac{\sinh \left(x\right)}{\cosh \left(x\right)}\right)$$
15	1 8 14	cmpt	$$class\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sinh \left(x\right)}{\cosh \left(x\right)}\right)$$
16	0 15	wceq	$$wff\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sinh \left(x\right)}{\cosh \left(x\right)}\right)$$