Metamath Proof Explorer

Theorem coshalfpi

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

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

Proof

Step Hyp Ref Expression
1 sinhalfpilem 
 |-  ( ( sin ` ( _pi / 2 ) ) = 1 /\ ( cos ` ( _pi / 2 ) ) = 0 )
2 1 simpri 
 |-  ( cos ` ( _pi / 2 ) ) = 0