Metamath Proof Explorer

Theorem sin2pim

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

Ref Expression
Assertion sin2pim ⊢ A ∈ ℂ → sin ⁡ 2 ⁢ π − A = − sin ⁡ A

Proof

Step Hyp Ref Expression
1 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
2 1z ⊢ 1 ∈ ℤ
3 sinper ⊢ − A ∈ ℂ ∧ 1 ∈ ℤ → sin ⁡ - A + 1 ⁢ 2 ⁢ π = sin ⁡ − A
4 1 2 3 sylancl ⊢ A ∈ ℂ → sin ⁡ - A + 1 ⁢ 2 ⁢ π = sin ⁡ − 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 ∈ ℂ → sin ⁡ - A + 1 ⁢ 2 ⁢ π = sin ⁡ 2 ⁢ π − A
16 4 15 eqtr3d ⊢ A ∈ ℂ → sin ⁡ − A = sin ⁡ 2 ⁢ π − A
17 sinneg ⊢ A ∈ ℂ → sin ⁡ − A = − sin ⁡ A
18 16 17 eqtr3d ⊢ A ∈ ℂ → sin ⁡ 2 ⁢ π − A = − sin ⁡ A