Metamath Proof Explorer


Theorem tanhval-named

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 ) )

Proof

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 ) )