Description: The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishlg.p | |
|
ishlg.i | |
||
ishlg.k | |
||
ishlg.a | |
||
ishlg.b | |
||
ishlg.c | |
||
ishlg.g | |
||
hlcomd.1 | |
||
Assertion | hlne1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishlg.p | |
|
2 | ishlg.i | |
|
3 | ishlg.k | |
|
4 | ishlg.a | |
|
5 | ishlg.b | |
|
6 | ishlg.c | |
|
7 | ishlg.g | |
|
8 | hlcomd.1 | |
|
9 | 1 2 3 4 5 6 7 | ishlg | |
10 | 8 9 | mpbid | |
11 | 10 | simp1d | |