Theorem cosneg

Description: The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005)

	Ref	Expression
Assertion	cosneg	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negicn	⊢ - i ∈ ℂ
2		mulcl	⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
4		efcl	⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
5	3 4	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
6		ax-icn	⊢ i ∈ ℂ
7		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
8	6 7	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
9		efcl	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
10	8 9	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
11		mulneg12	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
12	6 11	mpan	⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
13	12	eqcomd	⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = ( - i · 𝐴 ) )
14	13	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
15		mul2neg	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · - 𝐴 ) = ( i · 𝐴 ) )
16	6 15	mpan	⊢ ( 𝐴 ∈ ℂ → ( - i · - 𝐴 ) = ( i · 𝐴 ) )
17	16	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · - 𝐴 ) ) = ( exp ‘ ( i · 𝐴 ) ) )
18	14 17	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) + ( exp ‘ ( i · 𝐴 ) ) ) )
19	5 10 18	comraddd	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) )
20	19	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
21		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
22		cosval	⊢ ( - 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) / 2 ) )
23	21 22	syl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) / 2 ) )
24		cosval	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
25	20 23 24	3eqtr4d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )