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 = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( tan ` ( _i x. x ) ) / _i ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctanh	|- tanh
1		vx	|- x
2		ccosh	|- cosh
3	2	ccnv	|- `' cosh
4		cc	|- CC
5		cc0	|- 0
6	5	csn	|- { 0 }
7	4 6	cdif	|- ( CC \ { 0 } )
8	3 7	cima	|- ( `' cosh " ( CC \ { 0 } ) )
9		ctan	|- tan
10		ci	|- _i
11		cmul	|- x.
12	1	cv	|- x
13	10 12 11	co	|- ( _i x. x )
14	13 9	cfv	|- ( tan ` ( _i x. x ) )
15		cdiv	|- /
16	14 10 15	co	|- ( ( tan ` ( _i x. x ) ) / _i )
17	1 8 16	cmpt	|- ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( tan ` ( _i x. x ) ) / _i ) )
18	0 17	wceq	|- tanh = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( tan ` ( _i x. x ) ) / _i ) )