Theorem tanh0

Description: Value of the tanh function at 0. (Contributed by Jon Pennant, 22-Oct-2026)

	Ref	Expression
Assertion	tanh0	$$⊢\tanh \left(0\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		cosh0	$$⊢\cosh \left(0\right)=1$$
3		ax-1ne0	$$⊢1\ne 0$$
4	2 3	eqnetri	$$⊢\cosh \left(0\right)\ne 0$$
5		tanhval	$$⊢\left(0\in ℂ\wedge \cosh \left(0\right)\ne 0\right)\to \tanh \left(0\right)=\frac{\sinh \left(0\right)}{\cosh \left(0\right)}$$
6	1 4 5	mp2an	$$⊢\tanh \left(0\right)=\frac{\sinh \left(0\right)}{\cosh \left(0\right)}$$
7		sinh0	$$⊢\sinh \left(0\right)=0$$
8	7	oveq1i	$$⊢\frac{\sinh \left(0\right)}{\cosh \left(0\right)}=\frac{0}{\cosh \left(0\right)}$$
9		ax-1cn	$$⊢1\in ℂ$$
10	2 9	eqeltri	$$⊢\cosh \left(0\right)\in ℂ$$
11	10 4	div0i	$$⊢\frac{0}{\cosh \left(0\right)}=0$$
12	6 8 11	3eqtri	$$⊢\tanh \left(0\right)=0$$