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 ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 2 · π ) − 𝐴 ) ) = - ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 negcl ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
2 1z 1 ∈ ℤ
3 sinper ( ( - 𝐴 ∈ ℂ ∧ 1 ∈ ℤ ) → ( sin ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( sin ‘ - 𝐴 ) )
4 1 2 3 sylancl ( 𝐴 ∈ ℂ → ( sin ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( sin ‘ - 𝐴 ) )
5 2cn 2 ∈ ℂ
6 picn π ∈ ℂ
7 5 6 mulcli ( 2 · π ) ∈ ℂ
8 7 mulid2i ( 1 · ( 2 · π ) ) = ( 2 · π )
9 8 oveq2i ( - 𝐴 + ( 1 · ( 2 · π ) ) ) = ( - 𝐴 + ( 2 · π ) )
10 negsubdi ( ( 𝐴 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → - ( 𝐴 − ( 2 · π ) ) = ( - 𝐴 + ( 2 · π ) ) )
11 negsubdi2 ( ( 𝐴 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → - ( 𝐴 − ( 2 · π ) ) = ( ( 2 · π ) − 𝐴 ) )
12 10 11 eqtr3d ( ( 𝐴 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → ( - 𝐴 + ( 2 · π ) ) = ( ( 2 · π ) − 𝐴 ) )
13 7 12 mpan2 ( 𝐴 ∈ ℂ → ( - 𝐴 + ( 2 · π ) ) = ( ( 2 · π ) − 𝐴 ) )
14 9 13 syl5eq ( 𝐴 ∈ ℂ → ( - 𝐴 + ( 1 · ( 2 · π ) ) ) = ( ( 2 · π ) − 𝐴 ) )
15 14 fveq2d ( 𝐴 ∈ ℂ → ( sin ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 2 · π ) − 𝐴 ) ) )
16 4 15 eqtr3d ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = ( sin ‘ ( ( 2 · π ) − 𝐴 ) ) )
17 sinneg ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = - ( sin ‘ 𝐴 ) )
18 16 17 eqtr3d ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 2 · π ) − 𝐴 ) ) = - ( sin ‘ 𝐴 ) )