Metamath Proof Explorer

Theorem sinh0

Description: Value of the sinh function at 0. (Contributed by Jon Pennant, 9-Sep-2026)

Ref Expression
Assertion sinh0 
|- ( sinh ` 0 ) = 0

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 sinhval-named 
 |-  ( 0 e. CC -> ( sinh ` 0 ) = ( ( sin ` ( _i x. 0 ) ) / _i ) )
3 1 2 ax-mp 
 |-  ( sinh ` 0 ) = ( ( sin ` ( _i x. 0 ) ) / _i )
4 it0e0 
 |-  ( _i x. 0 ) = 0
5 4 fveq2i 
 |-  ( sin ` ( _i x. 0 ) ) = ( sin ` 0 )
6 sin0 
 |-  ( sin ` 0 ) = 0
7 5 6 eqtri 
 |-  ( sin ` ( _i x. 0 ) ) = 0
8 7 oveq1i 
 |-  ( ( sin ` ( _i x. 0 ) ) / _i ) = ( 0 / _i )
9 ax-icn 
 |-  _i e. CC
10 ine0 
 |-  _i =/= 0
11 9 10 div0i 
 |-  ( 0 / _i ) = 0
12 3 8 11 3eqtri 
 |-  ( sinh ` 0 ) = 0