This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
2 1z ⊢ 1 ∈ ℤ
3 cosper ⊢ ( ( - 𝐴 ∈ ℂ ∧ 1 ∈ ℤ ) → ( cos ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( cos ‘ - 𝐴 ) )
4 1 2 3 sylancl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( cos ‘ - 𝐴 ) )
5 2cn ⊢ 2 ∈ ℂ
6 picn ⊢ π ∈ ℂ
7 5 6 mulcli ⊢ ( 2 · π ) ∈ ℂ
8 7 mullidi ⊢ ( 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 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 + ( 1 · ( 2 · π ) ) ) = ( ( 2 · π ) − 𝐴 ) )
15 14 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( cos ‘ ( ( 2 · π ) − 𝐴 ) ) )
16 4 15 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ ( ( 2 · π ) − 𝐴 ) ) )
17 cosneg ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
18 16 17 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( 2 · π ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )