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 \in 𝑸 \land B \in 𝑸) \to (A <_{𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$

Proof

Step	Hyp	Ref	Expression
1		brinxp	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑝𝑸} B \leftrightarrow A (<_{𝑝𝑸} \cap (𝑸 \times 𝑸)) B)$
2		df-ltnq	$⊢ <_{𝑸} = <_{𝑝𝑸} \cap (𝑸 \times 𝑸)$
3	2	breqi	$⊢ A <_{𝑸} B \leftrightarrow A (<_{𝑝𝑸} \cap (𝑸 \times 𝑸)) B$
4	1 3	bitr4di	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑝𝑸} B \leftrightarrow A <_{𝑸} B)$
5		relxp	$⊢ Rel (𝑵 \times 𝑵)$
6		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
7		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
8	5 6 7	sylancr	$⊢ A \in 𝑸 \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
9		elpqn	$⊢ B \in 𝑸 \to B \in (𝑵 \times 𝑵)$
10		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
11	5 9 10	sylancr	$⊢ B \in 𝑸 \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
12	8 11	breqan12d	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑝𝑸} B \leftrightarrow ⟨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)⟩ \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
14	12 13	bitrdi	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑝𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
15	4 14	bitr3d	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$