Theorem coshneg

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

	Ref	Expression
Assertion	coshneg	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cosh ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
2		coshval-named	⊢ ( - 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cos ‘ ( i · - 𝐴 ) ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cos ‘ ( i · - 𝐴 ) ) )
4		ax-icn	⊢ i ∈ ℂ
5		mulcl	⊢ ( ( i ∈ ℂ ∧ - 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) ∈ ℂ )
6	4 1 5	sylancr	⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) ∈ ℂ )
7		cosneg	⊢ ( ( i · - 𝐴 ) ∈ ℂ → ( cos ‘ - ( i · - 𝐴 ) ) = ( cos ‘ ( i · - 𝐴 ) ) )
8	6 7	syl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - ( i · - 𝐴 ) ) = ( cos ‘ ( i · - 𝐴 ) ) )
9	3 8	eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cos ‘ - ( i · - 𝐴 ) ) )
10	4	a1i	⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
11		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
12	10 11	mulneg2d	⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
13	12	negeqd	⊢ ( 𝐴 ∈ ℂ → - ( i · - 𝐴 ) = - - ( i · 𝐴 ) )
14	10 11	mulcld	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
15	14	negnegd	⊢ ( 𝐴 ∈ ℂ → - - ( i · 𝐴 ) = ( i · 𝐴 ) )
16	13 15	eqtrd	⊢ ( 𝐴 ∈ ℂ → - ( i · - 𝐴 ) = ( i · 𝐴 ) )
17	16	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - ( i · - 𝐴 ) ) = ( cos ‘ ( i · 𝐴 ) ) )
18	9 17	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
19		coshval-named	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
20	18 19	eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ - 𝐴 ) = ( cosh ‘ 𝐴 ) )