Description: Value of the named tanh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-tanh . (Contributed by David A. Wheeler, 10-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tanhval-named | |- ( A e. ( `' cosh " ( CC \ { 0 } ) ) -> ( tanh ` A ) = ( ( tan ` ( _i x. A ) ) / _i ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq2 | |- ( x = A -> ( _i x. x ) = ( _i x. A ) ) |
|
| 2 | 1 | fveq2d | |- ( x = A -> ( tan ` ( _i x. x ) ) = ( tan ` ( _i x. A ) ) ) |
| 3 | 2 | oveq1d | |- ( x = A -> ( ( tan ` ( _i x. x ) ) / _i ) = ( ( tan ` ( _i x. A ) ) / _i ) ) |
| 4 | df-tanh | |- tanh = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( tan ` ( _i x. x ) ) / _i ) ) |
|
| 5 | ovex | |- ( ( tan ` ( _i x. A ) ) / _i ) e. _V |
|
| 6 | 3 4 5 | fvmpt | |- ( A e. ( `' cosh " ( CC \ { 0 } ) ) -> ( tanh ` A ) = ( ( tan ` ( _i x. A ) ) / _i ) ) |