Theorem coshneg

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

	Ref	Expression
Assertion	coshneg	|- ( A e. CC -> ( cosh ` -u A ) = ( cosh ` A ) )

Proof

Step	Hyp	Ref	Expression
1		negcl	|- ( A e. CC -> -u A e. CC )
2		coshval-named	|- ( -u A e. CC -> ( cosh ` -u A ) = ( cos ` ( _i x. -u A ) ) )
3	1 2	syl	|- ( A e. CC -> ( cosh ` -u A ) = ( cos ` ( _i x. -u A ) ) )
4		ax-icn	|- _i e. CC
5		mulcl	|- ( ( _i e. CC /\ -u A e. CC ) -> ( _i x. -u A ) e. CC )
6	4 1 5	sylancr	|- ( A e. CC -> ( _i x. -u A ) e. CC )
7		cosneg	|- ( ( _i x. -u A ) e. CC -> ( cos ` -u ( _i x. -u A ) ) = ( cos ` ( _i x. -u A ) ) )
8	6 7	syl	|- ( A e. CC -> ( cos ` -u ( _i x. -u A ) ) = ( cos ` ( _i x. -u A ) ) )
9	3 8	eqtr4d	|- ( A e. CC -> ( cosh ` -u A ) = ( cos ` -u ( _i x. -u A ) ) )
10	4	a1i	|- ( A e. CC -> _i e. CC )
11		id	|- ( A e. CC -> A e. CC )
12	10 11	mulneg2d	|- ( A e. CC -> ( _i x. -u A ) = -u ( _i x. A ) )
13	12	negeqd	|- ( A e. CC -> -u ( _i x. -u A ) = -u -u ( _i x. A ) )
14	10 11	mulcld	|- ( A e. CC -> ( _i x. A ) e. CC )
15	14	negnegd	|- ( A e. CC -> -u -u ( _i x. A ) = ( _i x. A ) )
16	13 15	eqtrd	|- ( A e. CC -> -u ( _i x. -u A ) = ( _i x. A ) )
17	16	fveq2d	|- ( A e. CC -> ( cos ` -u ( _i x. -u A ) ) = ( cos ` ( _i x. A ) ) )
18	9 17	eqtrd	|- ( A e. CC -> ( cosh ` -u A ) = ( cos ` ( _i x. A ) ) )
19		coshval-named	|- ( A e. CC -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
20	18 19	eqtr4d	|- ( A e. CC -> ( cosh ` -u A ) = ( cosh ` A ) )