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 π 2 = 0

Proof

Step Hyp Ref Expression
1 sinhalfpilem sin π 2 = 1 cos π 2 = 0
2 1 simpri cos π 2 = 0