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