Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
reneg1lt0
Next ⟩
sn-inelr
Metamath Proof Explorer
Ascii
Unicode
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