Theorem tanh0

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

	Ref	Expression
Assertion	tanh0	⊢ ( tanh ‘ 0 ) = 0

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		cosh0	⊢ ( cosh ‘ 0 ) = 1
3		ax-1ne0	⊢ 1 ≠ 0
4	2 3	eqnetri	⊢ ( cosh ‘ 0 ) ≠ 0
5		tanhval	⊢ ( ( 0 ∈ ℂ ∧ ( cosh ‘ 0 ) ≠ 0 ) → ( tanh ‘ 0 ) = ( ( sinh ‘ 0 ) / ( cosh ‘ 0 ) ) )
6	1 4 5	mp2an	⊢ ( tanh ‘ 0 ) = ( ( sinh ‘ 0 ) / ( cosh ‘ 0 ) )
7		sinh0	⊢ ( sinh ‘ 0 ) = 0
8	7	oveq1i	⊢ ( ( sinh ‘ 0 ) / ( cosh ‘ 0 ) ) = ( 0 / ( cosh ‘ 0 ) )
9		ax-1cn	⊢ 1 ∈ ℂ
10	2 9	eqeltri	⊢ ( cosh ‘ 0 ) ∈ ℂ
11	10 4	div0i	⊢ ( 0 / ( cosh ‘ 0 ) ) = 0
12	6 8 11	3eqtri	⊢ ( tanh ‘ 0 ) = 0