Metamath Proof Explorer


Theorem pine0

Description: _pi is nonzero. (Contributed by SN, 25-Apr-2025)

Ref Expression
Assertion pine0 π 0

Proof

Step Hyp Ref Expression
1 pire π
2 pipos 0 < π
3 1 2 gt0ne0ii π 0