Theorem tanhf

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

	Ref	Expression
Assertion	tanhf	⊢ tanh : ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-tanh	⊢ tanh = ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) ) )
2		coshf	⊢ cosh : ℂ ⟶ ℂ
3		ffn	⊢ ( cosh : ℂ ⟶ ℂ → cosh Fn ℂ )
4		elpreima	⊢ ( cosh Fn ℂ → ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( cosh ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
5	2 3 4	mp2b	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( cosh ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
6	5	simplbi	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
7		sinhcl	⊢ ( 𝑥 ∈ ℂ → ( sinh ‘ 𝑥 ) ∈ ℂ )
8	6 7	syl	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( sinh ‘ 𝑥 ) ∈ ℂ )
9		coshcl	⊢ ( 𝑥 ∈ ℂ → ( cosh ‘ 𝑥 ) ∈ ℂ )
10	6 9	syl	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( cosh ‘ 𝑥 ) ∈ ℂ )
11	5	simprbi	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( cosh ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
12	11	eldifsnbd	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( cosh ‘ 𝑥 ) ≠ 0 )
13	8 10 12	divcld	⊢ ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) ) ∈ ℂ )
14	1 13	fmpti	⊢ tanh : ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ⟶ ℂ