Metamath Proof Explorer

Theorem tanhcl

Description: The closure of the tanh function with complex argument. (Contributed by Jon Pennant, 9-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 coshcl 
 |-  ( A e. CC -> ( cosh ` A ) e. CC )
2 1 adantr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) e. CC )
3 simpr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) =/= 0 )
4 2 3 eldifsnd 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) e. ( CC \ { 0 } ) )
5 coshf 
 |-  cosh : CC --> CC
6 ffn 
 |-  ( cosh : CC --> CC -> cosh Fn CC )
7 elpreima 
 |-  ( cosh Fn CC -> ( A e. ( `' cosh " ( CC \ { 0 } ) ) <-> ( A e. CC /\ ( cosh ` A ) e. ( CC \ { 0 } ) ) ) )
8 5 6 7 mp2b 
 |-  ( A e. ( `' cosh " ( CC \ { 0 } ) ) <-> ( A e. CC /\ ( cosh ` A ) e. ( CC \ { 0 } ) ) )
9 tanhf 
 |-  tanh : ( `' cosh " ( CC \ { 0 } ) ) --> CC
10 9 ffvelcdmi 
 |-  ( A e. ( `' cosh " ( CC \ { 0 } ) ) -> ( tanh ` A ) e. CC )
11 8 10 sylbir 
 |-  ( ( A e. CC /\ ( cosh ` A ) e. ( CC \ { 0 } ) ) -> ( tanh ` A ) e. CC )
12 4 11 syldan 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) e. CC )