Metamath Proof Explorer

Theorem cosh0

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

Ref Expression
Assertion cosh0 
|- ( cosh ` 0 ) = 1

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 coshval-named 
 |-  ( 0 e. CC -> ( cosh ` 0 ) = ( cos ` ( _i x. 0 ) ) )
3 1 2 ax-mp 
 |-  ( cosh ` 0 ) = ( cos ` ( _i x. 0 ) )
4 it0e0 
 |-  ( _i x. 0 ) = 0
5 4 fveq2i 
 |-  ( cos ` ( _i x. 0 ) ) = ( cos ` 0 )
6 cos0 
 |-  ( cos ` 0 ) = 1
7 3 5 6 3eqtri 
 |-  ( cosh ` 0 ) = 1