Metamath Proof Explorer


Theorem sinpi

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

Ref Expression
Assertion sinpi ⊢ sin ⁡ π = 0

Proof

Step Hyp Ref Expression
1 pilem3 ⊢ π ∈ 2 4 ∧ sin ⁡ π = 0
2 1 simpri ⊢ sin ⁡ π = 0