Metamath Proof Explorer

Theorem lterpq

Description: Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013) (New usage is discouraged.)

Ref Expression
Assertion lterpq ⊢A<𝑝𝑸B↔/𝑸⁡A<𝑸/𝑸⁡B

Proof

Step Hyp Ref Expression
1 df-ltpq ⊢<𝑝𝑸=xy|x∈𝑵×𝑵∧y∈𝑵×𝑵∧1st⁡x⋅𝑵2nd⁡y<𝑵1st⁡y⋅𝑵2nd⁡x
2 opabssxp ⊢xy|x∈𝑵×𝑵∧y∈𝑵×𝑵∧1st⁡x⋅𝑵2nd⁡y<𝑵1st⁡y⋅𝑵2nd⁡x⊆𝑵×𝑵×𝑵×𝑵
3 1 2 eqsstri ⊢<𝑝𝑸⊆𝑵×𝑵×𝑵×𝑵
4 3 brel ⊢A<𝑝𝑸B→A∈𝑵×𝑵∧B∈𝑵×𝑵
5 ltrelnq ⊢<𝑸⊆𝑸×𝑸
6 5 brel ⊢/𝑸⁡A<𝑸/𝑸⁡B→/𝑸⁡A∈𝑸∧/𝑸⁡B∈𝑸
7 elpqn ⊢/𝑸⁡A∈𝑸→/𝑸⁡A∈𝑵×𝑵
8 elpqn ⊢/𝑸⁡B∈𝑸→/𝑸⁡B∈𝑵×𝑵
9 nqerf ⊢/𝑸:𝑵×𝑵⟶𝑸
10 9 fdmi ⊢dom⁡/𝑸=𝑵×𝑵
11 0nelxp ⊢¬∅∈𝑵×𝑵
12 10 11 ndmfvrcl ⊢/𝑸⁡A∈𝑵×𝑵→A∈𝑵×𝑵
13 10 11 ndmfvrcl ⊢/𝑸⁡B∈𝑵×𝑵→B∈𝑵×𝑵
14 12 13 anim12i ⊢/𝑸⁡A∈𝑵×𝑵∧/𝑸⁡B∈𝑵×𝑵→A∈𝑵×𝑵∧B∈𝑵×𝑵
15 7 8 14 syl2an ⊢/𝑸⁡A∈𝑸∧/𝑸⁡B∈𝑸→A∈𝑵×𝑵∧B∈𝑵×𝑵
16 6 15 syl ⊢/𝑸⁡A<𝑸/𝑸⁡B→A∈𝑵×𝑵∧B∈𝑵×𝑵
17 xp1st ⊢A∈𝑵×𝑵→1st⁡A∈𝑵
18 xp2nd ⊢B∈𝑵×𝑵→2nd⁡B∈𝑵
19 mulclpi ⊢1st⁡A∈𝑵∧2nd⁡B∈𝑵→1st⁡A⋅𝑵2nd⁡B∈𝑵
20 17 18 19 syl2an ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡A⋅𝑵2nd⁡B∈𝑵
21 ltmpi ⊢1st⁡A⋅𝑵2nd⁡B∈𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A↔1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
22 20 21 syl ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A↔1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
23 nqercl ⊢A∈𝑵×𝑵→/𝑸⁡A∈𝑸
24 nqercl ⊢B∈𝑵×𝑵→/𝑸⁡B∈𝑸
25 ordpinq ⊢/𝑸⁡A∈𝑸∧/𝑸⁡B∈𝑸→/𝑸⁡A<𝑸/𝑸⁡B↔1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
26 23 24 25 syl2an ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→/𝑸⁡A<𝑸/𝑸⁡B↔1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
27 1st2nd2 ⊢A∈𝑵×𝑵→A=1st⁡A2nd⁡A
28 1st2nd2 ⊢B∈𝑵×𝑵→B=1st⁡B2nd⁡B
29 27 28 breqan12d ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→A<𝑝𝑸B↔1st⁡A2nd⁡A<𝑝𝑸1st⁡B2nd⁡B
30 ordpipq ⊢1st⁡A2nd⁡A<𝑝𝑸1st⁡B2nd⁡B↔1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A
31 29 30 bitrdi ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→A<𝑝𝑸B↔1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A
32 xp1st ⊢/𝑸⁡A∈𝑵×𝑵→1st⁡/𝑸⁡A∈𝑵
33 23 7 32 3syl ⊢A∈𝑵×𝑵→1st⁡/𝑸⁡A∈𝑵
34 xp2nd ⊢/𝑸⁡B∈𝑵×𝑵→2nd⁡/𝑸⁡B∈𝑵
35 24 8 34 3syl ⊢B∈𝑵×𝑵→2nd⁡/𝑸⁡B∈𝑵
36 mulclpi ⊢1st⁡/𝑸⁡A∈𝑵∧2nd⁡/𝑸⁡B∈𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B∈𝑵
37 33 35 36 syl2an ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B∈𝑵
38 ltmpi ⊢1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B∈𝑵→1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A↔1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡B⋅𝑵2nd⁡A
39 37 38 syl ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A↔1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡B⋅𝑵2nd⁡A
40 mulcompi ⊢1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B
41 40 a1i ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B
42 nqerrel ⊢A∈𝑵×𝑵→A~𝑸/𝑸⁡A
43 23 7 syl ⊢A∈𝑵×𝑵→/𝑸⁡A∈𝑵×𝑵
44 enqbreq2 ⊢A∈𝑵×𝑵∧/𝑸⁡A∈𝑵×𝑵→A~𝑸/𝑸⁡A↔1st⁡A⋅𝑵2nd⁡/𝑸⁡A=1st⁡/𝑸⁡A⋅𝑵2nd⁡A
45 43 44 mpdan ⊢A∈𝑵×𝑵→A~𝑸/𝑸⁡A↔1st⁡A⋅𝑵2nd⁡/𝑸⁡A=1st⁡/𝑸⁡A⋅𝑵2nd⁡A
46 42 45 mpbid ⊢A∈𝑵×𝑵→1st⁡A⋅𝑵2nd⁡/𝑸⁡A=1st⁡/𝑸⁡A⋅𝑵2nd⁡A
47 46 eqcomd ⊢A∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡A=1st⁡A⋅𝑵2nd⁡/𝑸⁡A
48 nqerrel ⊢B∈𝑵×𝑵→B~𝑸/𝑸⁡B
49 24 8 syl ⊢B∈𝑵×𝑵→/𝑸⁡B∈𝑵×𝑵
50 enqbreq2 ⊢B∈𝑵×𝑵∧/𝑸⁡B∈𝑵×𝑵→B~𝑸/𝑸⁡B↔1st⁡B⋅𝑵2nd⁡/𝑸⁡B=1st⁡/𝑸⁡B⋅𝑵2nd⁡B
51 49 50 mpdan ⊢B∈𝑵×𝑵→B~𝑸/𝑸⁡B↔1st⁡B⋅𝑵2nd⁡/𝑸⁡B=1st⁡/𝑸⁡B⋅𝑵2nd⁡B
52 48 51 mpbid ⊢B∈𝑵×𝑵→1st⁡B⋅𝑵2nd⁡/𝑸⁡B=1st⁡/𝑸⁡B⋅𝑵2nd⁡B
53 47 52 oveqan12d ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B⋅𝑵2nd⁡/𝑸⁡B=1st⁡A⋅𝑵2nd⁡/𝑸⁡A⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡B
54 mulcompi ⊢1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡B⋅𝑵2nd⁡A=1st⁡B⋅𝑵2nd⁡A⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B
55 fvex ⊢1st⁡B∈V
56 fvex ⊢2nd⁡A∈V
57 fvex ⊢1st⁡/𝑸⁡A∈V
58 mulcompi ⊢x⋅𝑵y=y⋅𝑵x
59 mulasspi ⊢x⋅𝑵y⋅𝑵z=x⋅𝑵y⋅𝑵z
60 fvex ⊢2nd⁡/𝑸⁡B∈V
61 55 56 57 58 59 60 caov411 ⊢1st⁡B⋅𝑵2nd⁡A⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B=1st⁡/𝑸⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B⋅𝑵2nd⁡/𝑸⁡B
62 54 61 eqtri ⊢1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡B⋅𝑵2nd⁡A=1st⁡/𝑸⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B⋅𝑵2nd⁡/𝑸⁡B
63 mulcompi ⊢1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A=1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B
64 fvex ⊢1st⁡/𝑸⁡B∈V
65 fvex ⊢2nd⁡/𝑸⁡A∈V
66 fvex ⊢1st⁡A∈V
67 fvex ⊢2nd⁡B∈V
68 64 65 66 58 59 67 caov411 ⊢1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡/𝑸⁡A⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡B
69 63 68 eqtri ⊢1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A=1st⁡A⋅𝑵2nd⁡/𝑸⁡A⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡B
70 53 62 69 3eqtr4g ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡B⋅𝑵2nd⁡A=1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
71 41 70 breq12d ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B⋅𝑵1st⁡B⋅𝑵2nd⁡A↔1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
72 31 39 71 3bitrd ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→A<𝑝𝑸B↔1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡A⋅𝑵2nd⁡/𝑸⁡B<𝑵1st⁡A⋅𝑵2nd⁡B⋅𝑵1st⁡/𝑸⁡B⋅𝑵2nd⁡/𝑸⁡A
73 22 26 72 3bitr4rd ⊢A∈𝑵×𝑵∧B∈𝑵×𝑵→A<𝑝𝑸B↔/𝑸⁡A<𝑸/𝑸⁡B
74 4 16 73 pm5.21nii ⊢A<𝑝𝑸B↔/𝑸⁡A<𝑸/𝑸⁡B