Metamath Proof Explorer


Theorem reneg1lt0

Description: Lemma for sn-inelr . (Contributed by SN, 1-Jun-2024)

Ref Expression
Assertion reneg1lt0
|- ( 0 -R 1 ) < 0

Proof

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