Theorem cosnegpi

Description: The cosine of negative _pi is negative 1 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	cosnegpi	$$⊢\cos \left(-\mathrm{\pi }\right)=-1$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3	1 2	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
4	3	mulm1i	$$⊢-12\mathrm{\pi }=-2\mathrm{\pi }$$
5	4	oveq2i	$$⊢\mathrm{\pi }+-12\mathrm{\pi }=\mathrm{\pi }+\left(-2\mathrm{\pi }\right)$$
6	2 3	negsubi	$$⊢\mathrm{\pi }+\left(-2\mathrm{\pi }\right)=\mathrm{\pi }-2\mathrm{\pi }$$
7		sub2times	$$⊢\mathrm{\pi }\in ℂ\to \mathrm{\pi }-2\mathrm{\pi }=-\mathrm{\pi }$$
8	2 7	ax-mp	$$⊢\mathrm{\pi }-2\mathrm{\pi }=-\mathrm{\pi }$$
9	5 6 8	3eqtrri	$$⊢-\mathrm{\pi }=\mathrm{\pi }+-12\mathrm{\pi }$$
10	9	fveq2i	$$⊢\cos \left(-\mathrm{\pi }\right)=\cos \left(\mathrm{\pi }+-12\mathrm{\pi }\right)$$
11		neg1z	$$⊢-1\in \mathbb{Z}$$
12		cosper	$$⊢\left(\mathrm{\pi }\in ℂ\wedge -1\in \mathbb{Z}\right)\to \cos \left(\mathrm{\pi }+-12\mathrm{\pi }\right)=\cos \mathrm{\pi }$$
13	2 11 12	mp2an	$$⊢\cos \left(\mathrm{\pi }+-12\mathrm{\pi }\right)=\cos \mathrm{\pi }$$
14		cospi	$$⊢\cos \mathrm{\pi }=-1$$
15	10 13 14	3eqtri	$$⊢\cos \left(-\mathrm{\pi }\right)=-1$$