Database
REAL AND COMPLEX NUMBERS
Order sets
Infinity and the extended real number system (cont.)
xrltne
Next ⟩
nltpnft
Metamath Proof Explorer
Ascii
Unicode
Theorem
xrltne
Description:
'Less than' implies not equal for extended reals.
(Contributed by
NM
, 20-Jan-2006)
Ref
Expression
Assertion
xrltne
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
∧
A
<
B
→
B
≠
A
Proof
Step
Hyp
Ref
Expression
1
orc
⊢
A
<
B
→
A
<
B
∨
B
<
A
2
xrltso
⊢
<
Or
ℝ
*
3
sotrieq
⊢
<
Or
ℝ
*
∧
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
=
B
↔
¬
A
<
B
∨
B
<
A
4
2
3
mpan
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
=
B
↔
¬
A
<
B
∨
B
<
A
5
4
necon2abid
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
<
B
∨
B
<
A
↔
A
≠
B
6
1
5
syl5ib
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
A
<
B
→
A
≠
B
7
6
3impia
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
∧
A
<
B
→
A
≠
B
8
7
necomd
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
∧
A
<
B
→
B
≠
A