Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Properties of pi = 3.14159...
coshalfpi
Next ⟩
cosneghalfpi
Metamath Proof Explorer
Ascii
Unicode
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