Theorem cosneghalfpi

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

	Ref	Expression
Assertion	cosneghalfpi	$$⊢\cos \left(-\frac{\mathrm{\pi }}{2}\right)=0$$

Proof

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