Theorem coshalfpi

Description: The cosine of _pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008)

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

Proof

Step	Hyp	Ref	Expression
1		sinhalfpilem	⊢ ( ( sin ‘ ( π / 2 ) ) = 1 ∧ ( cos ‘ ( π / 2 ) ) = 0 )
2	1	simpri	⊢ ( cos ‘ ( π / 2 ) ) = 0