Metamath Proof Explorer

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 e. CC
2 cosh0 
 |-  ( cosh ` 0 ) = 1
3 ax-1ne0 
 |-  1 =/= 0
4 2 3 eqnetri 
 |-  ( cosh ` 0 ) =/= 0
5 tanhval 
 |-  ( ( 0 e. CC /\ ( 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 e. CC
10 2 9 eqeltri 
 |-  ( cosh ` 0 ) e. CC
11 10 4 div0i 
 |-  ( 0 / ( cosh ` 0 ) ) = 0
12 6 8 11 3eqtri 
 |-  ( tanh ` 0 ) = 0