Metamath Proof Explorer

Theorem pige0

Description: _pi is nonnegative. (Contributed by Umit Teoman Dogan, 10-Jun-2026)

Ref Expression
Assertion pige0 
|- 0 <_ _pi

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 pire 
 |-  _pi e. RR
3 pipos 
 |-  0 < _pi
4 1 2 3 ltleii 
 |-  0 <_ _pi