Theorem cosppi

Description: Cosine of a number plus _pi . (Contributed by NM, 18-Aug-2008)

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

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		cosadd	$$⊢\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	subid1d	$$⊢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$$