Theorem coshneg

Description: The cosh function is even. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Assertion	coshneg	$$⊢A\in ℂ\to \cosh \left(-A\right)=\cosh \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
2		coshval-named	$$⊢-A\in ℂ\to \cosh \left(-A\right)=\cos \mathrm{i}\left(-A\right)$$
3	1 2	syl	$$⊢A\in ℂ\to \cosh \left(-A\right)=\cos \mathrm{i}\left(-A\right)$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge -A\in ℂ\right)\to \mathrm{i}\left(-A\right)\in ℂ$$
6	4 1 5	sylancr	$$⊢A\in ℂ\to \mathrm{i}\left(-A\right)\in ℂ$$
7		cosneg	$$⊢\mathrm{i}\left(-A\right)\in ℂ\to \cos \left(-\mathrm{i}\left(-A\right)\right)=\cos \mathrm{i}\left(-A\right)$$
8	6 7	syl	$$⊢A\in ℂ\to \cos \left(-\mathrm{i}\left(-A\right)\right)=\cos \mathrm{i}\left(-A\right)$$
9	3 8	eqtr4d	$$⊢A\in ℂ\to \cosh \left(-A\right)=\cos \left(-\mathrm{i}\left(-A\right)\right)$$
10	4	a1i	$$⊢A\in ℂ\to \mathrm{i}\in ℂ$$
11		id	$$⊢A\in ℂ\to A\in ℂ$$
12	10 11	mulneg2d	$$⊢A\in ℂ\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
13	12	negeqd	$$⊢A\in ℂ\to -\mathrm{i}\left(-A\right)=-\left(-\mathrm{i}A\right)$$
14	10 11	mulcld	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
15	14	negnegd	$$⊢A\in ℂ\to -\left(-\mathrm{i}A\right)=\mathrm{i}A$$
16	13 15	eqtrd	$$⊢A\in ℂ\to -\mathrm{i}\left(-A\right)=\mathrm{i}A$$
17	16	fveq2d	$$⊢A\in ℂ\to \cos \left(-\mathrm{i}\left(-A\right)\right)=\cos \mathrm{i}A$$
18	9 17	eqtrd	$$⊢A\in ℂ\to \cosh \left(-A\right)=\cos \mathrm{i}A$$
19		coshval-named	$$⊢A\in ℂ\to \cosh \left(A\right)=\cos \mathrm{i}A$$
20	18 19	eqtr4d	$$⊢A\in ℂ\to \cosh \left(-A\right)=\cosh \left(A\right)$$