Description: Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of Gleason p. 120. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ltmnq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulnqf | |
|
2 | 1 | fdmi | |
3 | ltrelnq | |
|
4 | 0nnq | |
|
5 | elpqn | |
|
6 | 5 | 3ad2ant3 | |
7 | xp1st | |
|
8 | 6 7 | syl | |
9 | xp2nd | |
|
10 | 6 9 | syl | |
11 | mulclpi | |
|
12 | 8 10 11 | syl2anc | |
13 | ltmpi | |
|
14 | 12 13 | syl | |
15 | fvex | |
|
16 | fvex | |
|
17 | fvex | |
|
18 | mulcompi | |
|
19 | mulasspi | |
|
20 | fvex | |
|
21 | 15 16 17 18 19 20 | caov4 | |
22 | fvex | |
|
23 | fvex | |
|
24 | 15 16 22 18 19 23 | caov4 | |
25 | 21 24 | breq12i | |
26 | 14 25 | bitrdi | |
27 | ordpipq | |
|
28 | 26 27 | bitr4di | |
29 | elpqn | |
|
30 | 29 | 3ad2ant1 | |
31 | mulpipq2 | |
|
32 | 6 30 31 | syl2anc | |
33 | elpqn | |
|
34 | 33 | 3ad2ant2 | |
35 | mulpipq2 | |
|
36 | 6 34 35 | syl2anc | |
37 | 32 36 | breq12d | |
38 | 28 37 | bitr4d | |
39 | ordpinq | |
|
40 | 39 | 3adant3 | |
41 | mulpqnq | |
|
42 | 41 | ancoms | |
43 | 42 | 3adant2 | |
44 | mulpqnq | |
|
45 | 44 | ancoms | |
46 | 45 | 3adant1 | |
47 | 43 46 | breq12d | |
48 | lterpq | |
|
49 | 47 48 | bitr4di | |
50 | 38 40 49 | 3bitr4d | |
51 | 2 3 4 50 | ndmovord | |