Metamath Proof Explorer

Theorem ordpipq

Description: Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ordpipq ( ⟨ 𝐴 , 𝐵 ⟩ <pQ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
2 opex ⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
3 eleq1 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑥 ∈ ( N × N ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ) )
4 3 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ) )
5 4 anbi1d ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) ) )
6 fveq2 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
7 opelxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ↔ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) )
8 op1stg ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
9 7 8 sylbi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
10 9 adantr ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
11 6 10 sylan9eq ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ) → ( 1st ‘ 𝑥 ) = 𝐴 )
12 11 oveq1d ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ) → ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) )
13 fveq2 ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
14 op2ndg ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
15 7 14 sylbi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
16 15 adantr ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
17 13 16 sylan9eq ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ) → ( 2nd ‘ 𝑥 ) = 𝐵 )
18 17 oveq2d ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ) → ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) = ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) )
19 12 18 breq12d ⊢ ( ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ) → ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ↔ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) )
20 19 pm5.32da ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) ) )
21 5 20 bitrd ⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) ) )
22 eleq1 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑦 ∈ ( N × N ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) )
23 22 anbi2d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ) )
24 23 anbi1d ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) ) )
25 fveq2 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 2nd ‘ 𝑦 ) = ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
26 opelxp ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ↔ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) )
27 op2ndg ⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
28 26 27 sylbi ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
29 28 adantl ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
30 25 29 sylan9eq ⊢ ( ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ) → ( 2nd ‘ 𝑦 ) = 𝐷 )
31 30 oveq2d ⊢ ( ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ) → ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) = ( 𝐴 ·N 𝐷 ) )
32 fveq2 ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 1st ‘ 𝑦 ) = ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
33 op1stg ⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
34 26 33 sylbi ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
35 34 adantl ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
36 32 35 sylan9eq ⊢ ( ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ) → ( 1st ‘ 𝑦 ) = 𝐶 )
37 36 oveq1d ⊢ ( ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ) → ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) = ( 𝐶 ·N 𝐵 ) )
38 31 37 breq12d ⊢ ( ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ) → ( ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ↔ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) )
39 38 pm5.32da ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) ) )
40 24 39 bitrd ⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( 𝐴 ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N 𝐵 ) ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) ) )
41 df-ltpq ⊢ <pQ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) ∧ ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) <N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) }
42 1 2 21 40 41 brab ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ <pQ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) )
43 simpr ⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) → ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) )
44 ltrelpi ⊢ <N ⊆ ( N × N )
45 44 brel ⊢ ( ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) → ( ( 𝐴 ·N 𝐷 ) ∈ N ∧ ( 𝐶 ·N 𝐵 ) ∈ N ) )
46 dmmulpi ⊢ dom ·N = ( N × N )
47 0npi ⊢ ¬ ∅ ∈ N
48 46 47 ndmovrcl ⊢ ( ( 𝐴 ·N 𝐷 ) ∈ N → ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) )
49 46 47 ndmovrcl ⊢ ( ( 𝐶 ·N 𝐵 ) ∈ N → ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) )
50 48 49 anim12i ⊢ ( ( ( 𝐴 ·N 𝐷 ) ∈ N ∧ ( 𝐶 ·N 𝐵 ) ∈ N ) → ( ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) )
51 opelxpi ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) )
52 51 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) )
53 simprl ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → 𝐶 ∈ N )
54 simplr ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → 𝐷 ∈ N )
55 53 54 opelxpd ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) )
56 52 55 jca ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐷 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) )
57 45 50 56 3syl ⊢ ( ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) )
58 57 ancri ⊢ ( ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) )
59 43 58 impbii ⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) ∧ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) ) ↔ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) )
60 42 59 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ <pQ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ·N 𝐷 ) <N ( 𝐶 ·N 𝐵 ) )