Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltmnq Unicode version

Theorem ltmnq 8838
 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.)
Assertion
Ref Expression
ltmnq

Proof of Theorem ltmnq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulnqf 8815 . . 3
21fdmi 5587 . 2
3 ltrelnq 8792 . 2
4 0nnq 8790 . 2
5 elpqn 8791 . . . . . . . . . 10
653ad2ant3 980 . . . . . . . . 9
7 xp1st 6367 . . . . . . . . 9
86, 7syl 16 . . . . . . . 8
9 xp2nd 6368 . . . . . . . . 9
106, 9syl 16 . . . . . . . 8
11 mulclpi 8759 . . . . . . . 8
128, 10, 11syl2anc 643 . . . . . . 7
13 ltmpi 8770 . . . . . . 7
1412, 13syl 16 . . . . . 6
15 fvex 5733 . . . . . . . 8
16 fvex 5733 . . . . . . . 8
17 fvex 5733 . . . . . . . 8
18 mulcompi 8762 . . . . . . . 8
19 mulasspi 8763 . . . . . . . 8
20 fvex 5733 . . . . . . . 8
2115, 16, 17, 18, 19, 20caov4 6269 . . . . . . 7
22 fvex 5733 . . . . . . . 8
23 fvex 5733 . . . . . . . 8
2415, 16, 22, 18, 19, 23caov4 6269 . . . . . . 7
2521, 24breq12i 4213 . . . . . 6
2614, 25syl6bb 253 . . . . 5
27 ordpipq 8808 . . . . 5
2826, 27syl6bbr 255 . . . 4
29 elpqn 8791 . . . . . . 7
30293ad2ant1 978 . . . . . 6
31 mulpipq2 8805 . . . . . 6
326, 30, 31syl2anc 643 . . . . 5
33 elpqn 8791 . . . . . . 7
34333ad2ant2 979 . . . . . 6
35 mulpipq2 8805 . . . . . 6
366, 34, 35syl2anc 643 . . . . 5
3732, 36breq12d 4217 . . . 4
3828, 37bitr4d 248 . . 3
39 ordpinq 8809 . . . 4