Metamath Proof Explorer

Theorem tanhval

Description: Value of the tanh function in terms of sinh and cosh. (Contributed by Jon Pennant, 22-Oct-2026)

Ref Expression
Assertion tanhval 
|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( sinh ` A ) / ( cosh ` A ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> A e. CC )
2 coshcl 
 |-  ( A e. CC -> ( cosh ` A ) e. CC )
3 2 anim1i 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( cosh ` A ) e. CC /\ ( cosh ` A ) =/= 0 ) )
4 eldifsn 
 |-  ( ( cosh ` A ) e. ( CC \ { 0 } ) <-> ( ( cosh ` A ) e. CC /\ ( cosh ` A ) =/= 0 ) )
5 3 4 sylibr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) e. ( CC \ { 0 } ) )
6 coshf 
 |-  cosh : CC --> CC
7 ffn 
 |-  ( cosh : CC --> CC -> cosh Fn CC )
8 elpreima 
 |-  ( cosh Fn CC -> ( A e. ( `' cosh " ( CC \ { 0 } ) ) <-> ( A e. CC /\ ( cosh ` A ) e. ( CC \ { 0 } ) ) ) )
9 6 7 8 mp2b 
 |-  ( A e. ( `' cosh " ( CC \ { 0 } ) ) <-> ( A e. CC /\ ( cosh ` A ) e. ( CC \ { 0 } ) ) )
10 1 5 9 sylanbrc 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> A e. ( `' cosh " ( CC \ { 0 } ) ) )
11 fveq2 
 |-  ( x = A -> ( sinh ` x ) = ( sinh ` A ) )
12 fveq2 
 |-  ( x = A -> ( cosh ` x ) = ( cosh ` A ) )
13 11 12 oveq12d 
 |-  ( x = A -> ( ( sinh ` x ) / ( cosh ` x ) ) = ( ( sinh ` A ) / ( cosh ` A ) ) )
14 df-tanh 
 |-  tanh = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( sinh ` x ) / ( cosh ` x ) ) )
15 ovex 
 |-  ( ( sinh ` A ) / ( cosh ` A ) ) e. _V
16 13 14 15 fvmpt 
 |-  ( A e. ( `' cosh " ( CC \ { 0 } ) ) -> ( tanh ` A ) = ( ( sinh ` A ) / ( cosh ` A ) ) )
17 10 16 syl 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( sinh ` A ) / ( cosh ` A ) ) )