Metamath Proof Explorer

Theorem cos2pim

Description: Cosine of a number subtracted from 2 x. _pi . (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion cos2pim ⊢ A ∈ ℂ → cos ⁡ 2 ⁢ π − A = cos ⁡ A

Proof

Step Hyp Ref Expression
1 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
2 1z ⊢ 1 ∈ ℤ
3 cosper ⊢ − A ∈ ℂ ∧ 1 ∈ ℤ → cos ⁡ - A + 1 ⁢ 2 ⁢ π = cos ⁡ − A
4 1 2 3 sylancl ⊢ A ∈ ℂ → cos ⁡ - A + 1 ⁢ 2 ⁢ π = cos ⁡ − A
5 2cn ⊢ 2 ∈ ℂ
6 picn ⊢ π ∈ ℂ
7 5 6 mulcli ⊢ 2 ⁢ π ∈ ℂ
8 7 mulid2i ⊢ 1 ⁢ 2 ⁢ π = 2 ⁢ π
9 8 oveq2i ⊢ - A + 1 ⁢ 2 ⁢ π = - A + 2 ⁢ π
10 negsubdi ⊢ A ∈ ℂ ∧ 2 ⁢ π ∈ ℂ → − A − 2 ⁢ π = - A + 2 ⁢ π
11 negsubdi2 ⊢ A ∈ ℂ ∧ 2 ⁢ π ∈ ℂ → − A − 2 ⁢ π = 2 ⁢ π − A
12 10 11 eqtr3d ⊢ A ∈ ℂ ∧ 2 ⁢ π ∈ ℂ → - A + 2 ⁢ π = 2 ⁢ π − A
13 7 12 mpan2 ⊢ A ∈ ℂ → - A + 2 ⁢ π = 2 ⁢ π − A
14 9 13 eqtrid ⊢ A ∈ ℂ → - A + 1 ⁢ 2 ⁢ π = 2 ⁢ π − A
15 14 fveq2d ⊢ A ∈ ℂ → cos ⁡ - A + 1 ⁢ 2 ⁢ π = cos ⁡ 2 ⁢ π − A
16 4 15 eqtr3d ⊢ A ∈ ℂ → cos ⁡ − A = cos ⁡ 2 ⁢ π − A
17 cosneg ⊢ A ∈ ℂ → cos ⁡ − A = cos ⁡ A
18 16 17 eqtr3d ⊢ A ∈ ℂ → cos ⁡ 2 ⁢ π − A = cos ⁡ A