Metamath Proof Explorer

Theorem cosneg

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

Ref Expression
Assertion cosneg ⊢A∈ℂ→cos⁡−A=cos⁡A

Proof

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