Metamath Proof Explorer

Theorem tanhf

Description: Domain and codomain of the tanh function. (Contributed by Jon Pennant, 22-Oct-2026)

Ref Expression
Assertion tanhf 
|- tanh : ( `' cosh " ( CC \ { 0 } ) ) --> CC

Proof

Step Hyp Ref Expression
1 df-tanh 
 |-  tanh = ( x e. ( `' cosh " ( CC \ { 0 } ) ) |-> ( ( sinh ` x ) / ( cosh ` x ) ) )
2 coshf 
 |-  cosh : CC --> CC
3 ffn 
 |-  ( cosh : CC --> CC -> cosh Fn CC )
4 elpreima 
 |-  ( cosh Fn CC -> ( x e. ( `' cosh " ( CC \ { 0 } ) ) <-> ( x e. CC /\ ( cosh ` x ) e. ( CC \ { 0 } ) ) ) )
5 2 3 4 mp2b 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) <-> ( x e. CC /\ ( cosh ` x ) e. ( CC \ { 0 } ) ) )
6 5 simplbi 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) -> x e. CC )
7 sinhcl 
 |-  ( x e. CC -> ( sinh ` x ) e. CC )
8 6 7 syl 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) -> ( sinh ` x ) e. CC )
9 coshcl 
 |-  ( x e. CC -> ( cosh ` x ) e. CC )
10 6 9 syl 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) -> ( cosh ` x ) e. CC )
11 5 simprbi 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) -> ( cosh ` x ) e. ( CC \ { 0 } ) )
12 11 eldifsnbd 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) -> ( cosh ` x ) =/= 0 )
13 8 10 12 divcld 
 |-  ( x e. ( `' cosh " ( CC \ { 0 } ) ) -> ( ( sinh ` x ) / ( cosh ` x ) ) e. CC )
14 1 13 fmpti 
 |-  tanh : ( `' cosh " ( CC \ { 0 } ) ) --> CC