Theorem cospi

Description: The cosine of _pi is -u 1 . (Contributed by Paul Chapman, 23-Jan-2008)

	Ref	Expression
Assertion	cospi	$$⊢\cos \mathrm{\pi }=-1$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		2cn	$$⊢2\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4	1 2 3	divcli	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
5		cos2t	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to \cos 2\left(\frac{\mathrm{\pi }}{2}\right)=2{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2-1$$
6	4 5	ax-mp	$$⊢\cos 2\left(\frac{\mathrm{\pi }}{2}\right)=2{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2-1$$
7	1 2 3	divcan2i	$$⊢2\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }$$
8	7	fveq2i	$$⊢\cos 2\left(\frac{\mathrm{\pi }}{2}\right)=\cos \mathrm{\pi }$$
9		coshalfpi	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
10	9	oveq1i	$$⊢{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=0^2$$
11		sq0	$$⊢0^2=0$$
12	10 11	eqtri	$$⊢{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=0$$
13	12	oveq2i	$$⊢2{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=2\cdot 0$$
14		2t0e0	$$⊢2\cdot 0=0$$
15	13 14	eqtri	$$⊢2{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2=0$$
16	15	oveq1i	$$⊢2{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2-1=0-1$$
17		df-neg	$$⊢-1=0-1$$
18	16 17	eqtr4i	$$⊢2{\cos \left(\frac{\mathrm{\pi }}{2}\right)}^2-1=-1$$
19	6 8 18	3eqtr3i	$$⊢\cos \mathrm{\pi }=-1$$