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	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
2		coshcl	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
3	2	anim1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( cosh ‘ 𝐴 ) ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) )
4		eldifsn	⊢ ( ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( cosh ‘ 𝐴 ) ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) )
5	3 4	sylibr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) )
6		coshf	⊢ cosh : ℂ ⟶ ℂ
7		ffn	⊢ ( cosh : ℂ ⟶ ℂ → cosh Fn ℂ )
8		elpreima	⊢ ( cosh Fn ℂ → ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
9	6 7 8	mp2b	⊢ ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) )
10	1 5 9	sylanbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) )
11		fveq2	⊢ ( 𝑥 = 𝐴 → ( sinh ‘ 𝑥 ) = ( sinh ‘ 𝐴 ) )
12		fveq2	⊢ ( 𝑥 = 𝐴 → ( cosh ‘ 𝑥 ) = ( cosh ‘ 𝐴 ) )
13	11 12	oveq12d	⊢ ( 𝑥 = 𝐴 → ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
14		df-tanh	⊢ tanh = ( 𝑥 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sinh ‘ 𝑥 ) / ( cosh ‘ 𝑥 ) ) )
15		ovex	⊢ ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) ∈ V
16	13 14 15	fvmpt	⊢ ( 𝐴 ∈ ( ◡ cosh “ ( ℂ ∖ { 0 } ) ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
17	10 16	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )