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	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(A\right)=\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to A\in ℂ$$
2		coshcl	$$⊢A\in ℂ\to \cosh \left(A\right)\in ℂ$$
3	2	anim1i	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \left(\cosh \left(A\right)\in ℂ\wedge \cosh \left(A\right)\ne 0\right)$$
4		eldifsn	$$⊢\cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(\cosh \left(A\right)\in ℂ\wedge \cosh \left(A\right)\ne 0\right)$$
5	3 4	sylibr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
6		coshf	$$⊢\cosh :ℂ⟶ℂ$$
7		ffn	$$⊢\cosh :ℂ⟶ℂ\to \cosh Fnℂ$$
8		elpreima	$$⊢\cosh Fnℂ\to \left(A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
9	6 7 8	mp2b	$$⊢A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge \cosh \left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
10	1 5 9	sylanbrc	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
11		fveq2	$$⊢x=A\to \sinh \left(x\right)=\sinh \left(A\right)$$
12		fveq2	$$⊢x=A\to \cosh \left(x\right)=\cosh \left(A\right)$$
13	11 12	oveq12d	$$⊢x=A\to \frac{\sinh \left(x\right)}{\cosh \left(x\right)}=\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$
14		df-tanh	$$⊢\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sinh \left(x\right)}{\cosh \left(x\right)}\right)$$
15		ovex	$$⊢\frac{\sinh \left(A\right)}{\cosh \left(A\right)}\in \mathrm{V}$$
16	13 14 15	fvmpt	$$⊢A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \tanh \left(A\right)=\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$
17	10 16	syl	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(A\right)=\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$