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 ∈ ℂ → e i ⁢ A ∈ ℂ
10 8 9 syl ⊢ A ∈ ℂ → e i ⁢ 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 ∈ ℂ → e i ⁢ − 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 = e i ⁢ A
18 14 17 oveq12d ⊢ A ∈ ℂ → e i ⁢ − A + e − i ⁢ − A = e − i ⁢ A + e i ⁢ A
19 5 10 18 comraddd ⊢ A ∈ ℂ → e i ⁢ − A + e − i ⁢ − A = e i ⁢ A + e − i ⁢ A
20 19 oveq1d ⊢ A ∈ ℂ → e i ⁢ − A + e − i ⁢ − A 2 = e i ⁢ A + e − i ⁢ A 2
21 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
22 cosval ⊢ − A ∈ ℂ → cos ⁡ − A = e i ⁢ − A + e − i ⁢ − A 2
23 21 22 syl ⊢ A ∈ ℂ → cos ⁡ − A = e i ⁢ − A + e − i ⁢ − A 2
24 cosval ⊢ A ∈ ℂ → cos ⁡ A = e i ⁢ A + e − i ⁢ A 2
25 20 23 24 3eqtr4d ⊢ A ∈ ℂ → cos ⁡ − A = cos ⁡ A