Theorem sin2pim

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

	Ref	Expression
Assertion	sin2pim	$$⊢A\in ℂ\to \sin \left(2\mathrm{\pi }-A\right)=-\sin A$$

Proof

Step	Hyp	Ref	Expression
1		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		sinper	$$⊢\left(-A\in ℂ\wedge 1\in \mathbb{Z}\right)\to \sin \left(-A+12\mathrm{\pi }\right)=\sin \left(-A\right)$$
4	1 2 3	sylancl	$$⊢A\in ℂ\to \sin \left(-A+12\mathrm{\pi }\right)=\sin \left(-A\right)$$
5		2cn	$$⊢2\in ℂ$$
6		picn	$$⊢\mathrm{\pi }\in ℂ$$
7	5 6	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
8	7	mullidi	$$⊢12\mathrm{\pi }=2\mathrm{\pi }$$
9	8	oveq2i	$$⊢-A+12\mathrm{\pi }=-A+2\mathrm{\pi }$$
10		negsubdi	$$⊢\left(A\in ℂ\wedge 2\mathrm{\pi }\in ℂ\right)\to -\left(A-2\mathrm{\pi }\right)=-A+2\mathrm{\pi }$$
11		negsubdi2	$$⊢\left(A\in ℂ\wedge 2\mathrm{\pi }\in ℂ\right)\to -\left(A-2\mathrm{\pi }\right)=2\mathrm{\pi }-A$$
12	10 11	eqtr3d	$$⊢\left(A\in ℂ\wedge 2\mathrm{\pi }\in ℂ\right)\to -A+2\mathrm{\pi }=2\mathrm{\pi }-A$$
13	7 12	mpan2	$$⊢A\in ℂ\to -A+2\mathrm{\pi }=2\mathrm{\pi }-A$$
14	9 13	eqtrid	$$⊢A\in ℂ\to -A+12\mathrm{\pi }=2\mathrm{\pi }-A$$
15	14	fveq2d	$$⊢A\in ℂ\to \sin \left(-A+12\mathrm{\pi }\right)=\sin \left(2\mathrm{\pi }-A\right)$$
16	4 15	eqtr3d	$$⊢A\in ℂ\to \sin \left(-A\right)=\sin \left(2\mathrm{\pi }-A\right)$$
17		sinneg	$$⊢A\in ℂ\to \sin \left(-A\right)=-\sin A$$
18	16 17	eqtr3d	$$⊢A\in ℂ\to \sin \left(2\mathrm{\pi }-A\right)=-\sin A$$