This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pine0

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

Ref Expression
Assertion pine0 
|- _pi =/= 0

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 pipos 
 |-  0 < _pi
3 1 2 gt0ne0ii 
 |-  _pi =/= 0