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	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	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( - 𝐴 + ( 1 · ( 2 · π ) ) ) ) = ( cos ‘ ( ( 2 · π ) − 𝐴 ) ) )
16	4 15	eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ ( ( 2 · π ) − 𝐴 ) ) )
17		cosneg	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )
18	16 17	eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( 2 · π ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )