Metamath Proof Explorer

Theorem negpilt0

Description: Negative _pi is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion negpilt0 
|- -u _pi < 0

Proof

Step Hyp Ref Expression
1 pipos 
 |-  0 < _pi
2 pire 
 |-  _pi e. RR
3 lt0neg2 
 |-  ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) )
4 2 3 ax-mp 
 |-  ( 0 < _pi <-> -u _pi < 0 )
5 1 4 mpbi 
 |-  -u _pi < 0