Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-ltaddneg
Next ⟩
reposdif
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-ltaddneg
Description:
ltaddneg
without
ax-mulcom
.
(Contributed by
SN
, 25-Jan-2025)
Ref
Expression
Assertion
sn-ltaddneg
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
A
<
0
↔
B
+
A
<
B
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0
∈
ℝ
2
ltadd2
⊢
A
∈
ℝ
∧
0
∈
ℝ
∧
B
∈
ℝ
→
A
<
0
↔
B
+
A
<
B
+
0
3
1
2
mp3an2
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
A
<
0
↔
B
+
A
<
B
+
0
4
readdrid
⊢
B
∈
ℝ
→
B
+
0
=
B
5
4
adantl
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
B
+
0
=
B
6
5
breq2d
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
B
+
A
<
B
+
0
↔
B
+
A
<
B
7
3
6
bitrd
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
A
<
0
↔
B
+
A
<
B