Database
REAL AND COMPLEX NUMBERS
Order sets
Infinity and the extended real number system (cont.)
xltneg
Next ⟩
xleneg
Metamath Proof Explorer
Ascii
Unicode
Theorem
xltneg
Description:
Extended real version of
ltneg
.
(Contributed by
Mario Carneiro
, 20-Aug-2015)
Ref
Expression
Assertion
xltneg
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
<
B
↔
−
B
<
−
A
Proof
Step
Hyp
Ref
Expression
1
xltnegi
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
∧
A
<
B
→
−
B
<
−
A
2
1
3expia
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
<
B
→
−
B
<
−
A
3
xnegcl
⊢
B
∈
ℝ
*
→
−
B
∈
ℝ
*
4
xnegcl
⊢
A
∈
ℝ
*
→
−
A
∈
ℝ
*
5
xltnegi
⊢
−
B
∈
ℝ
*
∧
−
A
∈
ℝ
*
∧
−
B
<
−
A
→
−
−
A
<
−
−
B
6
5
3expia
⊢
−
B
∈
ℝ
*
∧
−
A
∈
ℝ
*
→
−
B
<
−
A
→
−
−
A
<
−
−
B
7
3
4
6
syl2anr
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
−
B
<
−
A
→
−
−
A
<
−
−
B
8
xnegneg
⊢
A
∈
ℝ
*
→
−
−
A
=
A
9
xnegneg
⊢
B
∈
ℝ
*
→
−
−
B
=
B
10
8
9
breqan12d
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
−
−
A
<
−
−
B
↔
A
<
B
11
7
10
sylibd
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
−
B
<
−
A
→
A
<
B
12
2
11
impbid
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
<
B
↔
−
B
<
−
A