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 | ⊢ ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( tanh ‘ 𝐴 ) = ( ( tan ‘ ( i · 𝐴 ) ) / i ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq2 | ⊢ ( 𝑥 = 𝐴 → ( i · 𝑥 ) = ( i · 𝐴 ) ) | |
| 2 | 1 | fveq2d | ⊢ ( 𝑥 = 𝐴 → ( tan ‘ ( i · 𝑥 ) ) = ( tan ‘ ( i · 𝐴 ) ) ) |
| 3 | 2 | oveq1d | ⊢ ( 𝑥 = 𝐴 → ( ( tan ‘ ( i · 𝑥 ) ) / i ) = ( ( tan ‘ ( i · 𝐴 ) ) / i ) ) |
| 4 | df-tanh | ⊢ tanh = ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( tan ‘ ( i · 𝑥 ) ) / i ) ) | |
| 5 | ovex | ⊢ ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ V | |
| 6 | 3 4 5 | fvmpt | ⊢ ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( tanh ‘ 𝐴 ) = ( ( tan ‘ ( i · 𝐴 ) ) / i ) ) |