Description: Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ltsopr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pssirr | |
|
2 | ltprord | |
|
3 | 1 2 | mtbiri | |
4 | 3 | anidms | |
5 | psstr | |
|
6 | ltprord | |
|
7 | 6 | 3adant3 | |
8 | ltprord | |
|
9 | 8 | 3adant1 | |
10 | 7 9 | anbi12d | |
11 | ltprord | |
|
12 | 11 | 3adant2 | |
13 | 10 12 | imbi12d | |
14 | 5 13 | mpbiri | |
15 | psslinpr | |
|
16 | biidd | |
|
17 | ltprord | |
|
18 | 17 | ancoms | |
19 | 6 16 18 | 3orbi123d | |
20 | 15 19 | mpbird | |
21 | 4 14 20 | issoi | |