Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordpinq Structured version   Visualization version   GIF version

Theorem ordpinq 10100
 Description: Ordering of positive fractions in terms of positive integers. (Contributed by NM, 13-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ordpinq ((𝐴Q𝐵Q) → (𝐴 <Q 𝐵 ↔ ((1st𝐴) ·N (2nd𝐵)) <N ((1st𝐵) ·N (2nd𝐴))))

Proof of Theorem ordpinq
StepHypRef Expression
1 brinxp 5428 . . 3 ((𝐴Q𝐵Q) → (𝐴 <pQ 𝐵𝐴( <pQ ∩ (Q × Q))𝐵))
2 df-ltnq 10075 . . . 4 <Q = ( <pQ ∩ (Q × Q))
32breqi 4892 . . 3 (𝐴 <Q 𝐵𝐴( <pQ ∩ (Q × Q))𝐵)
41, 3syl6bbr 281 . 2 ((𝐴Q𝐵Q) → (𝐴 <pQ 𝐵𝐴 <Q 𝐵))
5 relxp 5373 . . . . 5 Rel (N × N)
6 elpqn 10082 . . . . 5 (𝐴Q𝐴 ∈ (N × N))
7 1st2nd 7493 . . . . 5 ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
85, 6, 7sylancr 581 . . . 4 (𝐴Q𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
9 elpqn 10082 . . . . 5 (𝐵Q𝐵 ∈ (N × N))
10 1st2nd 7493 . . . . 5 ((Rel (N × N) ∧ 𝐵 ∈ (N × N)) → 𝐵 = ⟨(1st𝐵), (2nd𝐵)⟩)
115, 9, 10sylancr 581 . . . 4 (𝐵Q𝐵 = ⟨(1st𝐵), (2nd𝐵)⟩)
128, 11breqan12d 4902 . . 3 ((𝐴Q𝐵Q) → (𝐴 <pQ 𝐵 ↔ ⟨(1st𝐴), (2nd𝐴)⟩ <pQ ⟨(1st𝐵), (2nd𝐵)⟩))
13 ordpipq 10099 . . 3 (⟨(1st𝐴), (2nd𝐴)⟩ <pQ ⟨(1st𝐵), (2nd𝐵)⟩ ↔ ((1st𝐴) ·N (2nd𝐵)) <N ((1st𝐵) ·N (2nd𝐴)))
1412, 13syl6bb 279 . 2 ((𝐴Q𝐵Q) → (𝐴 <pQ 𝐵 ↔ ((1st𝐴) ·N (2nd𝐵)) <N ((1st𝐵) ·N (2nd𝐴))))
154, 14bitr3d 273 1 ((𝐴Q𝐵Q) → (𝐴 <Q 𝐵 ↔ ((1st𝐴) ·N (2nd𝐵)) <N ((1st𝐵) ·N (2nd𝐴))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107   ∩ cin 3791  ⟨cop 4404   class class class wbr 4886   × cxp 5353  Rel wrel 5360  ‘cfv 6135  (class class class)co 6922  1st c1st 7443  2nd c2nd 7444  Ncnpi 10001   ·N cmi 10003
 Copyright terms: Public domain W3C validator