This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cosneghalfpi

Description: The cosine of -u _pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017)

		Ref	Expression
	Assertion	cosneghalfpi	$⊢ \cos (- \frac{π}{2}) = 0$

Step	Hyp	Ref	Expression
1		halfpire	$⊢ \frac{π}{2} \in ℝ$
2	1	recni	$⊢ \frac{π}{2} \in ℂ$
3		cosneg	$⊢ \frac{π}{2} \in ℂ \to \cos (- \frac{π}{2}) = \cos (\frac{π}{2})$
4	2 3	ax-mp	$⊢ \cos (- \frac{π}{2}) = \cos (\frac{π}{2})$
5		coshalfpi	$⊢ \cos (\frac{π}{2}) = 0$
6	4 5	eqtri	$⊢ \cos (- \frac{π}{2}) = 0$