Theorem cosh0

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

	Ref	Expression
Assertion	cosh0	$$⊢\cosh \left(0\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		coshval-named	$$⊢0\in ℂ\to \cosh \left(0\right)=\cos \mathrm{i}\cdot 0$$
3	1 2	ax-mp	$$⊢\cosh \left(0\right)=\cos \mathrm{i}\cdot 0$$
4		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
5	4	fveq2i	$$⊢\cos \mathrm{i}\cdot 0=\cos 0$$
6		cos0	$$⊢\cos 0=1$$
7	3 5 6	3eqtri	$$⊢\cosh \left(0\right)=1$$