Theorem sinmpi

Description: Sine of a number less _pi . (Contributed by Paul Chapman, 15-Mar-2008)

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

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		sinsub	$$⊢\left(A\in ℂ\wedge \mathrm{\pi }\in ℂ\right)\to \sin \left(A-\mathrm{\pi }\right)=\sin A\cos \mathrm{\pi }-\cos A\sin \mathrm{\pi }$$
3	1 2	mpan2	$$⊢A\in ℂ\to \sin \left(A-\mathrm{\pi }\right)=\sin A\cos \mathrm{\pi }-\cos A\sin \mathrm{\pi }$$
4		cospi	$$⊢\cos \mathrm{\pi }=-1$$
5	4	oveq2i	$$⊢\sin A\cos \mathrm{\pi }=\sin A-1$$
6		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
7		neg1cn	$$⊢-1\in ℂ$$
8		mulcom	$$⊢\left(\sin A\in ℂ\wedge -1\in ℂ\right)\to \sin A-1=-1\sin A$$
9	7 8	mpan2	$$⊢\sin A\in ℂ\to \sin A-1=-1\sin A$$
10		mulm1	$$⊢\sin A\in ℂ\to -1\sin A=-\sin A$$
11	9 10	eqtrd	$$⊢\sin A\in ℂ\to \sin A-1=-\sin A$$
12	6 11	syl	$$⊢A\in ℂ\to \sin A-1=-\sin A$$
13	5 12	syl5eq	$$⊢A\in ℂ\to \sin A\cos \mathrm{\pi }=-\sin A$$
14		sinpi	$$⊢\sin \mathrm{\pi }=0$$
15	14	oveq2i	$$⊢\cos A\sin \mathrm{\pi }=\cos A\cdot 0$$
16		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
17	16	mul01d	$$⊢A\in ℂ\to \cos A\cdot 0=0$$
18	15 17	syl5eq	$$⊢A\in ℂ\to \cos A\sin \mathrm{\pi }=0$$
19	13 18	oveq12d	$$⊢A\in ℂ\to \sin A\cos \mathrm{\pi }-\cos A\sin \mathrm{\pi }=-\sin A-0$$
20	6	negcld	$$⊢A\in ℂ\to -\sin A\in ℂ$$
21	20	subid1d	$$⊢A\in ℂ\to -\sin A-0=-\sin A$$
22	19 21	eqtrd	$$⊢A\in ℂ\to \sin A\cos \mathrm{\pi }-\cos A\sin \mathrm{\pi }=-\sin A$$
23	3 22	eqtrd	$$⊢A\in ℂ\to \sin \left(A-\mathrm{\pi }\right)=-\sin A$$