Theorem cosneghalfpi

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

	Ref	Expression
Assertion	cosneghalfpi	⊢ ( cos ‘ - ( π / 2 ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		halfpire	⊢ ( π / 2 ) ∈ ℝ
2	1	recni	⊢ ( π / 2 ) ∈ ℂ
3		cosneg	⊢ ( ( π / 2 ) ∈ ℂ → ( cos ‘ - ( π / 2 ) ) = ( cos ‘ ( π / 2 ) ) )
4	2 3	ax-mp	⊢ ( cos ‘ - ( π / 2 ) ) = ( cos ‘ ( π / 2 ) )
5		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
6	4 5	eqtri	⊢ ( cos ‘ - ( π / 2 ) ) = 0