Metamath Proof Explorer

Theorem ordpinq

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.)

Ref Expression
Assertion ordpinq ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A

Proof

Step Hyp Ref Expression
1 brinxp ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑝𝑸 B ↔ A < 𝑝𝑸 ∩ 𝑸 × 𝑸 B
2 df-ltnq ⊢ < 𝑸 = < 𝑝𝑸 ∩ 𝑸 × 𝑸
3 2 breqi ⊢ A < 𝑸 B ↔ A < 𝑝𝑸 ∩ 𝑸 × 𝑸 B
4 1 3 bitr4di ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑝𝑸 B ↔ A < 𝑸 B
5 relxp ⊢ Rel ⁡ 𝑵 × 𝑵
6 elpqn ⊢ A ∈ 𝑸 → A ∈ 𝑵 × 𝑵
7 1st2nd ⊢ Rel ⁡ 𝑵 × 𝑵 ∧ A ∈ 𝑵 × 𝑵 → A = 1 st ⁡ A 2 nd ⁡ A
8 5 6 7 sylancr ⊢ A ∈ 𝑸 → A = 1 st ⁡ A 2 nd ⁡ A
9 elpqn ⊢ B ∈ 𝑸 → B ∈ 𝑵 × 𝑵
10 1st2nd ⊢ Rel ⁡ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → B = 1 st ⁡ B 2 nd ⁡ B
11 5 9 10 sylancr ⊢ B ∈ 𝑸 → B = 1 st ⁡ B 2 nd ⁡ B
12 8 11 breqan12d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑝𝑸 B ↔ 1 st ⁡ A 2 nd ⁡ A < 𝑝𝑸 1 st ⁡ B 2 nd ⁡ B
13 ordpipq ⊢ 1 st ⁡ A 2 nd ⁡ A < 𝑝𝑸 1 st ⁡ B 2 nd ⁡ B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
14 12 13 bitrdi ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑝𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
15 4 14 bitr3d ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A < 𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B < 𝑵 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A