Metamath Proof Explorer

Theorem neg1lt0

Description: -1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion neg1lt0 
|- -u 1 < 0

Proof

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