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)

	Ref	Expression
Assertion	df-tanh	$$⊢\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\tan \mathrm{i}x}{\mathrm{i}}\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		ctan	$$class\tan$$
10		ci	$$class\mathrm{i}$$
11		cmul	$$class\times$$
12	1	cv	$$setvarx$$
13	10 12 11	co	$$class\mathrm{i}x$$
14	13 9	cfv	$$class\tan \mathrm{i}x$$
15		cdiv	$$class÷$$
16	14 10 15	co	$$class\left(\frac{\tan \mathrm{i}x}{\mathrm{i}}\right)$$
17	1 8 16	cmpt	$$class\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\tan \mathrm{i}x}{\mathrm{i}}\right)$$
18	0 17	wceq	$$wff\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\tan \mathrm{i}x}{\mathrm{i}}\right)$$