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 ( 𝐴 <pQ 𝐵 ↔ ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-ltpq <pQ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st𝑥 ) ·N ( 2nd𝑦 ) ) <N ( ( 1st𝑦 ) ·N ( 2nd𝑥 ) ) ) }
2 opabssxp { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st𝑥 ) ·N ( 2nd𝑦 ) ) <N ( ( 1st𝑦 ) ·N ( 2nd𝑥 ) ) ) } ⊆ ( ( N × N ) × ( N × N ) )
3 1 2 eqsstri <pQ ⊆ ( ( N × N ) × ( N × N ) )
4 3 brel ( 𝐴 <pQ 𝐵 → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
5 ltrelnq <Q ⊆ ( Q × Q )
6 5 brel ( ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) → ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) )
7 elpqn ( ( [Q] ‘ 𝐴 ) ∈ Q → ( [Q] ‘ 𝐴 ) ∈ ( N × N ) )
8 elpqn ( ( [Q] ‘ 𝐵 ) ∈ Q → ( [Q] ‘ 𝐵 ) ∈ ( N × N ) )
9 nqerf [Q] : ( N × N ) ⟶ Q
10 9 fdmi dom [Q] = ( N × N )
11 0nelxp ¬ ∅ ∈ ( N × N )
12 10 11 ndmfvrcl ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → 𝐴 ∈ ( N × N ) )
13 10 11 ndmfvrcl ( ( [Q] ‘ 𝐵 ) ∈ ( N × N ) → 𝐵 ∈ ( N × N ) )
14 12 13 anim12i ( ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ∧ ( [Q] ‘ 𝐵 ) ∈ ( N × N ) ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
15 7 8 14 syl2an ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
16 6 15 syl ( ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
17 xp1st ( 𝐴 ∈ ( N × N ) → ( 1st𝐴 ) ∈ N )
18 xp2nd ( 𝐵 ∈ ( N × N ) → ( 2nd𝐵 ) ∈ N )
19 mulclpi ( ( ( 1st𝐴 ) ∈ N ∧ ( 2nd𝐵 ) ∈ N ) → ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ∈ N )
20 17 18 19 syl2an ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ∈ N )
21 ltmpi ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ∈ N → ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) <N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ↔ ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <N ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
22 20 21 syl ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) <N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ↔ ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <N ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
23 nqercl ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ Q )
24 nqercl ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ Q )
25 ordpinq ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) <N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) )
26 23 24 25 syl2an ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) <N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) )
27 1st2nd2 ( 𝐴 ∈ ( N × N ) → 𝐴 = ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ )
28 1st2nd2 ( 𝐵 ∈ ( N × N ) → 𝐵 = ⟨ ( 1st𝐵 ) , ( 2nd𝐵 ) ⟩ )
29 27 28 breqan12d ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <pQ 𝐵 ↔ ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ <pQ ⟨ ( 1st𝐵 ) , ( 2nd𝐵 ) ⟩ ) )
30 ordpipq ( ⟨ ( 1st𝐴 ) , ( 2nd𝐴 ) ⟩ <pQ ⟨ ( 1st𝐵 ) , ( 2nd𝐵 ) ⟩ ↔ ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) )
31 29 30 bitrdi ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <pQ 𝐵 ↔ ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) )
32 xp1st ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ∈ N )
33 23 7 32 3syl ( 𝐴 ∈ ( N × N ) → ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ∈ N )
34 xp2nd ( ( [Q] ‘ 𝐵 ) ∈ ( N × N ) → ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ N )
35 24 8 34 3syl ( 𝐵 ∈ ( N × N ) → ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ N )
36 mulclpi ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ∈ N ∧ ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ N ) → ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ∈ N )
37 33 35 36 syl2an ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ∈ N )
38 ltmpi ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ∈ N → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) )
39 37 38 syl ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) <N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ↔ ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ) )
40 mulcompi ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
41 40 a1i ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) )
42 nqerrel ( 𝐴 ∈ ( N × N ) → 𝐴 ~Q ( [Q] ‘ 𝐴 ) )
43 23 7 syl ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ ( N × N ) )
44 enqbreq2 ( ( 𝐴 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ) → ( 𝐴 ~Q ( [Q] ‘ 𝐴 ) ↔ ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) = ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) ) )
45 43 44 mpdan ( 𝐴 ∈ ( N × N ) → ( 𝐴 ~Q ( [Q] ‘ 𝐴 ) ↔ ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) = ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) ) )
46 42 45 mpbid ( 𝐴 ∈ ( N × N ) → ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) = ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) )
47 46 eqcomd ( 𝐴 ∈ ( N × N ) → ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) = ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) )
48 nqerrel ( 𝐵 ∈ ( N × N ) → 𝐵 ~Q ( [Q] ‘ 𝐵 ) )
49 24 8 syl ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ ( N × N ) )
50 enqbreq2 ( ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐵 ) ∈ ( N × N ) ) → ( 𝐵 ~Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1st𝐵 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) = ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd𝐵 ) ) ) )
51 49 50 mpdan ( 𝐵 ∈ ( N × N ) → ( 𝐵 ~Q ( [Q] ‘ 𝐵 ) ↔ ( ( 1st𝐵 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) = ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd𝐵 ) ) ) )
52 48 51 mpbid ( 𝐵 ∈ ( N × N ) → ( ( 1st𝐵 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) = ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd𝐵 ) ) )
53 47 52 oveqan12d ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd𝐵 ) ) ) )
54 mulcompi ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
55 fvex ( 1st𝐵 ) ∈ V
56 fvex ( 2nd𝐴 ) ∈ V
57 fvex ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ∈ V
58 mulcompi ( 𝑥 ·N 𝑦 ) = ( 𝑦 ·N 𝑥 )
59 mulasspi ( ( 𝑥 ·N 𝑦 ) ·N 𝑧 ) = ( 𝑥 ·N ( 𝑦 ·N 𝑧 ) )
60 fvex ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ∈ V
61 55 56 57 58 59 60 caov411 ( ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) = ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
62 54 61 eqtri ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd𝐴 ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) )
63 mulcompi ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) = ( ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) )
64 fvex ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ∈ V
65 fvex ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ∈ V
66 fvex ( 1st𝐴 ) ∈ V
67 fvex ( 2nd𝐵 ) ∈ V
68 64 65 66 58 59 67 caov411 ( ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd𝐵 ) ) )
69 63 68 eqtri ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd𝐵 ) ) )
70 53 62 69 3eqtr4g ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) = ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) )
71 41 70 breq12d ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ) <N ( ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ·N ( ( 1st𝐵 ) ·N ( 2nd𝐴 ) ) ) ↔ ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <N ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
72 31 39 71 3bitrd ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <pQ 𝐵 ↔ ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐴 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐵 ) ) ) ) <N ( ( ( 1st𝐴 ) ·N ( 2nd𝐵 ) ) ·N ( ( 1st ‘ ( [Q] ‘ 𝐵 ) ) ·N ( 2nd ‘ ( [Q] ‘ 𝐴 ) ) ) ) ) )
73 22 26 72 3bitr4rd ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 <pQ 𝐵 ↔ ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) ) )
74 4 16 73 pm5.21nii ( 𝐴 <pQ 𝐵 ↔ ( [Q] ‘ 𝐴 ) <Q ( [Q] ‘ 𝐵 ) )