cospi

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

		Ref	Expression
	Assertion	cospi	$⊢ \cos π = - 1$

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

Metamath Proof Explorer