Theorem cosmpi

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

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

Proof

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