Metamath Proof Explorer


Theorem ltsonq

Description: 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996) (Revised by Mario Carneiro, 4-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltsonq <𝑸Or𝑸

Proof

Step Hyp Ref Expression
1 elpqn x𝑸x𝑵×𝑵
2 1 adantr x𝑸y𝑸x𝑵×𝑵
3 xp1st x𝑵×𝑵1stx𝑵
4 2 3 syl x𝑸y𝑸1stx𝑵
5 elpqn y𝑸y𝑵×𝑵
6 5 adantl x𝑸y𝑸y𝑵×𝑵
7 xp2nd y𝑵×𝑵2ndy𝑵
8 6 7 syl x𝑸y𝑸2ndy𝑵
9 mulclpi 1stx𝑵2ndy𝑵1stx𝑵2ndy𝑵
10 4 8 9 syl2anc x𝑸y𝑸1stx𝑵2ndy𝑵
11 xp1st y𝑵×𝑵1sty𝑵
12 6 11 syl x𝑸y𝑸1sty𝑵
13 xp2nd x𝑵×𝑵2ndx𝑵
14 2 13 syl x𝑸y𝑸2ndx𝑵
15 mulclpi 1sty𝑵2ndx𝑵1sty𝑵2ndx𝑵
16 12 14 15 syl2anc x𝑸y𝑸1sty𝑵2ndx𝑵
17 ltsopi <𝑵Or𝑵
18 sotric <𝑵Or𝑵1stx𝑵2ndy𝑵1sty𝑵2ndx𝑵1stx𝑵2ndy<𝑵1sty𝑵2ndx¬1stx𝑵2ndy=1sty𝑵2ndx1sty𝑵2ndx<𝑵1stx𝑵2ndy
19 17 18 mpan 1stx𝑵2ndy𝑵1sty𝑵2ndx𝑵1stx𝑵2ndy<𝑵1sty𝑵2ndx¬1stx𝑵2ndy=1sty𝑵2ndx1sty𝑵2ndx<𝑵1stx𝑵2ndy
20 10 16 19 syl2anc x𝑸y𝑸1stx𝑵2ndy<𝑵1sty𝑵2ndx¬1stx𝑵2ndy=1sty𝑵2ndx1sty𝑵2ndx<𝑵1stx𝑵2ndy
21 ordpinq x𝑸y𝑸x<𝑸y1stx𝑵2ndy<𝑵1sty𝑵2ndx
22 fveq2 x=y1stx=1sty
23 fveq2 x=y2ndx=2ndy
24 23 eqcomd x=y2ndy=2ndx
25 22 24 oveq12d x=y1stx𝑵2ndy=1sty𝑵2ndx
26 enqbreq2 x𝑵×𝑵y𝑵×𝑵x~𝑸y1stx𝑵2ndy=1sty𝑵2ndx
27 1 5 26 syl2an x𝑸y𝑸x~𝑸y1stx𝑵2ndy=1sty𝑵2ndx
28 enqeq x𝑸y𝑸x~𝑸yx=y
29 28 3expia x𝑸y𝑸x~𝑸yx=y
30 27 29 sylbird x𝑸y𝑸1stx𝑵2ndy=1sty𝑵2ndxx=y
31 25 30 impbid2 x𝑸y𝑸x=y1stx𝑵2ndy=1sty𝑵2ndx
32 ordpinq y𝑸x𝑸y<𝑸x1sty𝑵2ndx<𝑵1stx𝑵2ndy
33 32 ancoms x𝑸y𝑸y<𝑸x1sty𝑵2ndx<𝑵1stx𝑵2ndy
34 31 33 orbi12d x𝑸y𝑸x=yy<𝑸x1stx𝑵2ndy=1sty𝑵2ndx1sty𝑵2ndx<𝑵1stx𝑵2ndy
35 34 notbid x𝑸y𝑸¬x=yy<𝑸x¬1stx𝑵2ndy=1sty𝑵2ndx1sty𝑵2ndx<𝑵1stx𝑵2ndy
36 20 21 35 3bitr4d x𝑸y𝑸x<𝑸y¬x=yy<𝑸x
37 21 3adant3 x𝑸y𝑸z𝑸x<𝑸y1stx𝑵2ndy<𝑵1sty𝑵2ndx
38 elpqn z𝑸z𝑵×𝑵
39 38 3ad2ant3 x𝑸y𝑸z𝑸z𝑵×𝑵
40 xp2nd z𝑵×𝑵2ndz𝑵
41 ltmpi 2ndz𝑵1stx𝑵2ndy<𝑵1sty𝑵2ndx2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx
42 39 40 41 3syl x𝑸y𝑸z𝑸1stx𝑵2ndy<𝑵1sty𝑵2ndx2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx
43 37 42 bitrd x𝑸y𝑸z𝑸x<𝑸y2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx
44 ordpinq y𝑸z𝑸y<𝑸z1sty𝑵2ndz<𝑵1stz𝑵2ndy
45 44 3adant1 x𝑸y𝑸z𝑸y<𝑸z1sty𝑵2ndz<𝑵1stz𝑵2ndy
46 1 3ad2ant1 x𝑸y𝑸z𝑸x𝑵×𝑵
47 ltmpi 2ndx𝑵1sty𝑵2ndz<𝑵1stz𝑵2ndy2ndx𝑵1sty𝑵2ndz<𝑵2ndx𝑵1stz𝑵2ndy
48 46 13 47 3syl x𝑸y𝑸z𝑸1sty𝑵2ndz<𝑵1stz𝑵2ndy2ndx𝑵1sty𝑵2ndz<𝑵2ndx𝑵1stz𝑵2ndy
49 45 48 bitrd x𝑸y𝑸z𝑸y<𝑸z2ndx𝑵1sty𝑵2ndz<𝑵2ndx𝑵1stz𝑵2ndy
50 43 49 anbi12d x𝑸y𝑸z𝑸x<𝑸yy<𝑸z2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx2ndx𝑵1sty𝑵2ndz<𝑵2ndx𝑵1stz𝑵2ndy
51 fvex 2ndxV
52 fvex 1styV
53 fvex 2ndzV
54 mulcompi r𝑵s=s𝑵r
55 mulasspi r𝑵s𝑵t=r𝑵s𝑵t
56 51 52 53 54 55 caov13 2ndx𝑵1sty𝑵2ndz=2ndz𝑵1sty𝑵2ndx
57 fvex 1stzV
58 fvex 2ndyV
59 51 57 58 54 55 caov13 2ndx𝑵1stz𝑵2ndy=2ndy𝑵1stz𝑵2ndx
60 56 59 breq12i 2ndx𝑵1sty𝑵2ndz<𝑵2ndx𝑵1stz𝑵2ndy2ndz𝑵1sty𝑵2ndx<𝑵2ndy𝑵1stz𝑵2ndx
61 fvex 1stxV
62 53 61 58 54 55 caov13 2ndz𝑵1stx𝑵2ndy=2ndy𝑵1stx𝑵2ndz
63 ltrelpi <𝑵𝑵×𝑵
64 17 63 sotri 2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx2ndz𝑵1sty𝑵2ndx<𝑵2ndy𝑵1stz𝑵2ndx2ndz𝑵1stx𝑵2ndy<𝑵2ndy𝑵1stz𝑵2ndx
65 62 64 eqbrtrrid 2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx2ndz𝑵1sty𝑵2ndx<𝑵2ndy𝑵1stz𝑵2ndx2ndy𝑵1stx𝑵2ndz<𝑵2ndy𝑵1stz𝑵2ndx
66 60 65 sylan2b 2ndz𝑵1stx𝑵2ndy<𝑵2ndz𝑵1sty𝑵2ndx2ndx𝑵1sty𝑵2ndz<𝑵2ndx𝑵1stz𝑵2ndy2ndy𝑵1stx𝑵2ndz<𝑵2ndy𝑵1stz𝑵2ndx
67 50 66 syl6bi x𝑸y𝑸z𝑸x<𝑸yy<𝑸z2ndy𝑵1stx𝑵2ndz<𝑵2ndy𝑵1stz𝑵2ndx
68 ordpinq x𝑸z𝑸x<𝑸z1stx𝑵2ndz<𝑵1stz𝑵2ndx
69 68 3adant2 x𝑸y𝑸z𝑸x<𝑸z1stx𝑵2ndz<𝑵1stz𝑵2ndx
70 5 3ad2ant2 x𝑸y𝑸z𝑸y𝑵×𝑵
71 ltmpi 2ndy𝑵1stx𝑵2ndz<𝑵1stz𝑵2ndx2ndy𝑵1stx𝑵2ndz<𝑵2ndy𝑵1stz𝑵2ndx
72 70 7 71 3syl x𝑸y𝑸z𝑸1stx𝑵2ndz<𝑵1stz𝑵2ndx2ndy𝑵1stx𝑵2ndz<𝑵2ndy𝑵1stz𝑵2ndx
73 69 72 bitrd x𝑸y𝑸z𝑸x<𝑸z2ndy𝑵1stx𝑵2ndz<𝑵2ndy𝑵1stz𝑵2ndx
74 67 73 sylibrd x𝑸y𝑸z𝑸x<𝑸yy<𝑸zx<𝑸z
75 36 74 isso2i <𝑸Or𝑸