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

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		csinh	⊢ sinh
10	1	cv	⊢ 𝑥
11	10 9	cfv	⊢ ( sinh ‘ 𝑥 )
12		cdiv	⊢ /
13	10 2	cfv	⊢ ( cosh ‘ 𝑥 )
14	11 13 12	co	⊢ ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) )
15	1 8 14	cmpt	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) ) )
16	0 15	wceq	⊢ tanh = ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) ) )