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 = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( sinh ` x ) / ( cosh ` x ) ) ) |
| 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 | csinh | |- sinh |
|
| 10 | 1 | cv | |- x |
| 11 | 10 9 | cfv | |- ( sinh ` x ) |
| 12 | cdiv | |- / |
|
| 13 | 10 2 | cfv | |- ( cosh ` x ) |
| 14 | 11 13 12 | co | |- ( ( sinh ` x ) / ( cosh ` x ) ) |
| 15 | 1 8 14 | cmpt | |- ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( sinh ` x ) / ( cosh ` x ) ) ) |
| 16 | 0 15 | wceq | |- tanh = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( sinh ` x ) / ( cosh ` x ) ) ) |