Metamath Proof Explorer


Theorem reneg1lt0

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

Ref Expression
Assertion reneg1lt0 0 - 1 < 0

Proof

Step Hyp Ref Expression
1 sn-0lt1 0 < 1
2 1re 1
3 relt0neg2 1 0 < 1 0 - 1 < 0
4 2 3 ax-mp 0 < 1 0 - 1 < 0
5 1 4 mpbi 0 - 1 < 0