Theorem tanhcl

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

	Ref	Expression
Assertion	tanhcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		coshcl	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ∈ ℂ )
3		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ≠ 0 )
4	2 3	eldifsnd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) )
5		coshf	⊢ cosh : ℂ ⟶ ℂ
6		ffn	⊢ ( cosh : ℂ ⟶ ℂ → cosh Fn ℂ )
7		elpreima	⊢ ( cosh Fn ℂ → ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
8	5 6 7	mp2b	⊢ ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) )
9		tanhf	⊢ tanh : ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ⟶ ℂ
10	9	ffvelcdmi	⊢ ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( tanh ‘ 𝐴 ) ∈ ℂ )
11	8 10	sylbir	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) → ( tanh ‘ 𝐴 ) ∈ ℂ )
12	4 11	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) ∈ ℂ )