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