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

Theorem ltmnq 9415
 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 9392 . . 3
21fdmi 5746 . 2
3 ltrelnq 9369 . 2
4 0nnq 9367 . 2
5 elpqn 9368 . . . . . . . . . 10
653ad2ant3 1053 . . . . . . . . 9
7 xp1st 6842 . . . . . . . . 9
86, 7syl 17 . . . . . . . 8
9 xp2nd 6843 . . . . . . . . 9
106, 9syl 17 . . . . . . . 8
11 mulclpi 9336 . . . . . . . 8
128, 10, 11syl2anc 673 . . . . . . 7
13 ltmpi 9347 . . . . . . 7
1412, 13syl 17 . . . . . 6
15 fvex 5889 . . . . . . . 8
16 fvex 5889 . . . . . . . 8
17 fvex 5889 . . . . . . . 8
18 mulcompi 9339 . . . . . . . 8
19 mulasspi 9340 . . . . . . . 8
20 fvex 5889 . . . . . . . 8
2115, 16, 17, 18, 19, 20caov4 6519 . . . . . . 7
22 fvex 5889 . . . . . . . 8
23 fvex 5889 . . . . . . . 8
2415, 16, 22, 18, 19, 23caov4 6519 . . . . . . 7
2521, 24breq12i 4404 . . . . . 6
2614, 25syl6bb 269 . . . . 5
27 ordpipq 9385 . . . . 5
2826, 27syl6bbr 271 . . . 4
29 elpqn 9368 . . . . . . 7
30293ad2ant1 1051 . . . . . 6
31 mulpipq2 9382 . . . . . 6
326, 30, 31syl2anc 673 . . . . 5
33 elpqn 9368 . . . . . . 7
34333ad2ant2 1052 . . . . . 6
35 mulpipq2 9382 . . . . . 6
366, 34, 35syl2anc 673 . . . . 5
3732, 36breq12d 4408 . . . 4
3828, 37bitr4d 264 . . 3
39 ordpinq 9386 . . . 4