Metamath Proof Explorer


Theorem ltmnq

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 C𝑸A<𝑸BC𝑸A<𝑸C𝑸B

Proof

Step Hyp Ref Expression
1 mulnqf 𝑸:𝑸×𝑸𝑸
2 1 fdmi dom𝑸=𝑸×𝑸
3 ltrelnq <𝑸𝑸×𝑸
4 0nnq ¬𝑸
5 elpqn C𝑸C𝑵×𝑵
6 5 3ad2ant3 A𝑸B𝑸C𝑸C𝑵×𝑵
7 xp1st C𝑵×𝑵1stC𝑵
8 6 7 syl A𝑸B𝑸C𝑸1stC𝑵
9 xp2nd C𝑵×𝑵2ndC𝑵
10 6 9 syl A𝑸B𝑸C𝑸2ndC𝑵
11 mulclpi 1stC𝑵2ndC𝑵1stC𝑵2ndC𝑵
12 8 10 11 syl2anc A𝑸B𝑸C𝑸1stC𝑵2ndC𝑵
13 ltmpi 1stC𝑵2ndC𝑵1stA𝑵2ndB<𝑵1stB𝑵2ndA1stC𝑵2ndC𝑵1stA𝑵2ndB<𝑵1stC𝑵2ndC𝑵1stB𝑵2ndA
14 12 13 syl A𝑸B𝑸C𝑸1stA𝑵2ndB<𝑵1stB𝑵2ndA1stC𝑵2ndC𝑵1stA𝑵2ndB<𝑵1stC𝑵2ndC𝑵1stB𝑵2ndA
15 fvex 1stCV
16 fvex 2ndCV
17 fvex 1stAV
18 mulcompi x𝑵y=y𝑵x
19 mulasspi x𝑵y𝑵z=x𝑵y𝑵z
20 fvex 2ndBV
21 15 16 17 18 19 20 caov4 1stC𝑵2ndC𝑵1stA𝑵2ndB=1stC𝑵1stA𝑵2ndC𝑵2ndB
22 fvex 1stBV
23 fvex 2ndAV
24 15 16 22 18 19 23 caov4 1stC𝑵2ndC𝑵1stB𝑵2ndA=1stC𝑵1stB𝑵2ndC𝑵2ndA
25 21 24 breq12i 1stC𝑵2ndC𝑵1stA𝑵2ndB<𝑵1stC𝑵2ndC𝑵1stB𝑵2ndA1stC𝑵1stA𝑵2ndC𝑵2ndB<𝑵1stC𝑵1stB𝑵2ndC𝑵2ndA
26 14 25 bitrdi A𝑸B𝑸C𝑸1stA𝑵2ndB<𝑵1stB𝑵2ndA1stC𝑵1stA𝑵2ndC𝑵2ndB<𝑵1stC𝑵1stB𝑵2ndC𝑵2ndA
27 ordpipq 1stC𝑵1stA2ndC𝑵2ndA<𝑝𝑸1stC𝑵1stB2ndC𝑵2ndB1stC𝑵1stA𝑵2ndC𝑵2ndB<𝑵1stC𝑵1stB𝑵2ndC𝑵2ndA
28 26 27 bitr4di A𝑸B𝑸C𝑸1stA𝑵2ndB<𝑵1stB𝑵2ndA1stC𝑵1stA2ndC𝑵2ndA<𝑝𝑸1stC𝑵1stB2ndC𝑵2ndB
29 elpqn A𝑸A𝑵×𝑵
30 29 3ad2ant1 A𝑸B𝑸C𝑸A𝑵×𝑵
31 mulpipq2 C𝑵×𝑵A𝑵×𝑵C𝑝𝑸A=1stC𝑵1stA2ndC𝑵2ndA
32 6 30 31 syl2anc A𝑸B𝑸C𝑸C𝑝𝑸A=1stC𝑵1stA2ndC𝑵2ndA
33 elpqn B𝑸B𝑵×𝑵
34 33 3ad2ant2 A𝑸B𝑸C𝑸B𝑵×𝑵
35 mulpipq2 C𝑵×𝑵B𝑵×𝑵C𝑝𝑸B=1stC𝑵1stB2ndC𝑵2ndB
36 6 34 35 syl2anc A𝑸B𝑸C𝑸C𝑝𝑸B=1stC𝑵1stB2ndC𝑵2ndB
37 32 36 breq12d A𝑸B𝑸C𝑸C𝑝𝑸A<𝑝𝑸C𝑝𝑸B1stC𝑵1stA2ndC𝑵2ndA<𝑝𝑸1stC𝑵1stB2ndC𝑵2ndB
38 28 37 bitr4d A𝑸B𝑸C𝑸1stA𝑵2ndB<𝑵1stB𝑵2ndAC𝑝𝑸A<𝑝𝑸C𝑝𝑸B
39 ordpinq A𝑸B𝑸A<𝑸B1stA𝑵2ndB<𝑵1stB𝑵2ndA
40 39 3adant3 A𝑸B𝑸C𝑸A<𝑸B1stA𝑵2ndB<𝑵1stB𝑵2ndA
41 mulpqnq C𝑸A𝑸C𝑸A=/𝑸C𝑝𝑸A
42 41 ancoms A𝑸C𝑸C𝑸A=/𝑸C𝑝𝑸A
43 42 3adant2 A𝑸B𝑸C𝑸C𝑸A=/𝑸C𝑝𝑸A
44 mulpqnq C𝑸B𝑸C𝑸B=/𝑸C𝑝𝑸B
45 44 ancoms B𝑸C𝑸C𝑸B=/𝑸C𝑝𝑸B
46 45 3adant1 A𝑸B𝑸C𝑸C𝑸B=/𝑸C𝑝𝑸B
47 43 46 breq12d A𝑸B𝑸C𝑸C𝑸A<𝑸C𝑸B/𝑸C𝑝𝑸A<𝑸/𝑸C𝑝𝑸B
48 lterpq C𝑝𝑸A<𝑝𝑸C𝑝𝑸B/𝑸C𝑝𝑸A<𝑸/𝑸C𝑝𝑸B
49 47 48 bitr4di A𝑸B𝑸C𝑸C𝑸A<𝑸C𝑸BC𝑝𝑸A<𝑝𝑸C𝑝𝑸B
50 38 40 49 3bitr4d A𝑸B𝑸C𝑸A<𝑸BC𝑸A<𝑸C𝑸B
51 2 3 4 50 ndmovord C𝑸A<𝑸BC𝑸A<𝑸C𝑸B