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 neg0 
 |-  -u 0 = 0
2 0lt1 
 |-  0 < 1
3 1 2 eqbrtri 
 |-  -u 0 < 1
4 1re 
 |-  1 e. RR
5 0re 
 |-  0 e. RR
6 4 5 ltnegcon1i 
 |-  ( -u 1 < 0 <-> -u 0 < 1 )
7 3 6 mpbir 
 |-  -u 1 < 0