Theorem cosneghalfpi

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

	Ref	Expression
Assertion	cosneghalfpi	|- ( cos ` -u ( _pi / 2 ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		halfpire	|- ( _pi / 2 ) e. RR
2	1	recni	|- ( _pi / 2 ) e. CC
3		cosneg	|- ( ( _pi / 2 ) e. CC -> ( cos ` -u ( _pi / 2 ) ) = ( cos ` ( _pi / 2 ) ) )
4	2 3	ax-mp	|- ( cos ` -u ( _pi / 2 ) ) = ( cos ` ( _pi / 2 ) )
5		coshalfpi	|- ( cos ` ( _pi / 2 ) ) = 0
6	4 5	eqtri	|- ( cos ` -u ( _pi / 2 ) ) = 0