Database
SURREAL NUMBERS
Surreal arithmetic
Negation and Subtraction
sltneg
Next ⟩
sleneg
Metamath Proof Explorer
Ascii
Unicode
Theorem
sltneg
Description:
Negative of both sides of surreal less-than.
(Contributed by
Scott Fenton
, 3-Feb-2025)
Ref
Expression
Assertion
sltneg
⊢
A
∈
No
∧
B
∈
No
→
A
<
s
B
↔
+
s
⁡
B
<
s
+
s
⁡
A
Proof
Step
Hyp
Ref
Expression
1
sltnegim
⊢
A
∈
No
∧
B
∈
No
→
A
<
s
B
→
+
s
⁡
B
<
s
+
s
⁡
A
2
negscl
⊢
B
∈
No
→
+
s
⁡
B
∈
No
3
negscl
⊢
A
∈
No
→
+
s
⁡
A
∈
No
4
sltnegim
⊢
+
s
⁡
B
∈
No
∧
+
s
⁡
A
∈
No
→
+
s
⁡
B
<
s
+
s
⁡
A
→
+
s
⁡
+
s
⁡
A
<
s
+
s
⁡
+
s
⁡
B
5
2
3
4
syl2anr
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
B
<
s
+
s
⁡
A
→
+
s
⁡
+
s
⁡
A
<
s
+
s
⁡
+
s
⁡
B
6
negnegs
⊢
A
∈
No
→
+
s
⁡
+
s
⁡
A
=
A
7
negnegs
⊢
B
∈
No
→
+
s
⁡
+
s
⁡
B
=
B
8
6
7
breqan12d
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
+
s
⁡
A
<
s
+
s
⁡
+
s
⁡
B
↔
A
<
s
B
9
5
8
sylibd
⊢
A
∈
No
∧
B
∈
No
→
+
s
⁡
B
<
s
+
s
⁡
A
→
A
<
s
B
10
1
9
impbid
⊢
A
∈
No
∧
B
∈
No
→
A
<
s
B
↔
+
s
⁡
B
<
s
+
s
⁡
A