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 = ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( tan ‘ ( i · 𝑥 ) ) / i ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctanh	⊢ tanh
1		vx	⊢ 𝑥
2		ccosh	⊢ cosh
3	2	ccnv	⊢ ◡ cosh
4		cc	⊢ ℂ
5		cc0	⊢ 0
6	5	csn	⊢ { 0 }
7	4 6	cdif	⊢ ( ℂ ∖ { 0 } )
8	3 7	cima	⊢ ( ◡ cosh “ ( ℂ ∖ { 0 } ) )
9		ctan	⊢ tan
10		ci	⊢ i
11		cmul	⊢ ·
12	1	cv	⊢ 𝑥
13	10 12 11	co	⊢ ( i · 𝑥 )
14	13 9	cfv	⊢ ( tan ‘ ( i · 𝑥 ) )
15		cdiv	⊢ /
16	14 10 15	co	⊢ ( ( tan ‘ ( i · 𝑥 ) ) / i )
17	1 8 16	cmpt	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( tan ‘ ( i · 𝑥 ) ) / i ) )
18	0 17	wceq	⊢ tanh = ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( tan ‘ ( i · 𝑥 ) ) / i ) )