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 ∈ ℂ
2		coshval-named	⊢ ( 0 ∈ ℂ → ( cosh ‘ 0 ) = ( cos ‘ ( i · 0 ) ) )
3	1 2	ax-mp	⊢ ( cosh ‘ 0 ) = ( cos ‘ ( i · 0 ) )
4		it0e0	⊢ ( i · 0 ) = 0
5	4	fveq2i	⊢ ( cos ‘ ( i · 0 ) ) = ( cos ‘ 0 )
6		cos0	⊢ ( cos ‘ 0 ) = 1
7	3 5 6	3eqtri	⊢ ( cosh ‘ 0 ) = 1