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	$⊢ ⟨A, B⟩ <_{𝑝𝑸} ⟨C, D⟩ \leftrightarrow (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨A, B⟩ \in V$
2		opex	$⊢ ⟨C, D⟩ \in V$
3		eleq1	$⊢ x = ⟨A, B⟩ \to (x \in (𝑵 \times 𝑵) \leftrightarrow ⟨A, B⟩ \in (𝑵 \times 𝑵))$
4	3	anbi1d	$⊢ x = ⟨A, B⟩ \to ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \leftrightarrow (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)))$
5	4	anbi1d	$⊢ x = ⟨A, B⟩ \to (((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))))$
6		fveq2	$⊢ x = ⟨A, B⟩ \to 1^{st} (x) = 1^{st} (⟨A, B⟩)$
7		opelxp	$⊢ ⟨A, B⟩ \in (𝑵 \times 𝑵) \leftrightarrow (A \in 𝑵 \land B \in 𝑵)$
8		op1stg	$⊢ (A \in 𝑵 \land B \in 𝑵) \to 1^{st} (⟨A, B⟩) = A$
9	7 8	sylbi	$⊢ ⟨A, B⟩ \in (𝑵 \times 𝑵) \to 1^{st} (⟨A, B⟩) = A$
10	9	adantr	$⊢ (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 1^{st} (⟨A, B⟩) = A$
11	6 10	sylan9eq	$⊢ (x = ⟨A, B⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵))) \to 1^{st} (x) = A$
12	11	oveq1d	$⊢ (x = ⟨A, B⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵))) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = A \cdot_{𝑵} 2^{nd} (y)$
13		fveq2	$⊢ x = ⟨A, B⟩ \to 2^{nd} (x) = 2^{nd} (⟨A, B⟩)$
14		op2ndg	$⊢ (A \in 𝑵 \land B \in 𝑵) \to 2^{nd} (⟨A, B⟩) = B$
15	7 14	sylbi	$⊢ ⟨A, B⟩ \in (𝑵 \times 𝑵) \to 2^{nd} (⟨A, B⟩) = B$
16	15	adantr	$⊢ (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 2^{nd} (⟨A, B⟩) = B$
17	13 16	sylan9eq	$⊢ (x = ⟨A, B⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵))) \to 2^{nd} (x) = B$
18	17	oveq2d	$⊢ (x = ⟨A, B⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵))) \to 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) = 1^{st} (y) \cdot_{𝑵} B$
19	12 18	breq12d	$⊢ (x = ⟨A, B⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵))) \to ((1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \leftrightarrow (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B))$
20	19	pm5.32da	$⊢ x = ⟨A, B⟩ \to (((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B)))$
21	5 20	bitrd	$⊢ x = ⟨A, B⟩ \to (((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x))) \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B)))$
22		eleq1	$⊢ y = ⟨C, D⟩ \to (y \in (𝑵 \times 𝑵) \leftrightarrow ⟨C, D⟩ \in (𝑵 \times 𝑵))$
23	22	anbi2d	$⊢ y = ⟨C, D⟩ \to ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \leftrightarrow (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)))$
24	23	anbi1d	$⊢ y = ⟨C, D⟩ \to (((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B)) \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B)))$
25		fveq2	$⊢ y = ⟨C, D⟩ \to 2^{nd} (y) = 2^{nd} (⟨C, D⟩)$
26		opelxp	$⊢ ⟨C, D⟩ \in (𝑵 \times 𝑵) \leftrightarrow (C \in 𝑵 \land D \in 𝑵)$
27		op2ndg	$⊢ (C \in 𝑵 \land D \in 𝑵) \to 2^{nd} (⟨C, D⟩) = D$
28	26 27	sylbi	$⊢ ⟨C, D⟩ \in (𝑵 \times 𝑵) \to 2^{nd} (⟨C, D⟩) = D$
29	28	adantl	$⊢ (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \to 2^{nd} (⟨C, D⟩) = D$
30	25 29	sylan9eq	$⊢ (y = ⟨C, D⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))) \to 2^{nd} (y) = D$
31	30	oveq2d	$⊢ (y = ⟨C, D⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))) \to A \cdot_{𝑵} 2^{nd} (y) = A \cdot_{𝑵} D$
32		fveq2	$⊢ y = ⟨C, D⟩ \to 1^{st} (y) = 1^{st} (⟨C, D⟩)$
33		op1stg	$⊢ (C \in 𝑵 \land D \in 𝑵) \to 1^{st} (⟨C, D⟩) = C$
34	26 33	sylbi	$⊢ ⟨C, D⟩ \in (𝑵 \times 𝑵) \to 1^{st} (⟨C, D⟩) = C$
35	34	adantl	$⊢ (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \to 1^{st} (⟨C, D⟩) = C$
36	32 35	sylan9eq	$⊢ (y = ⟨C, D⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))) \to 1^{st} (y) = C$
37	36	oveq1d	$⊢ (y = ⟨C, D⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))) \to 1^{st} (y) \cdot_{𝑵} B = C \cdot_{𝑵} B$
38	31 37	breq12d	$⊢ (y = ⟨C, D⟩ \land (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))) \to ((A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B) \leftrightarrow (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B))$
39	38	pm5.32da	$⊢ y = ⟨C, D⟩ \to (((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B)) \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)))$
40	24 39	bitrd	$⊢ y = ⟨C, D⟩ \to (((⟨A, B⟩ \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} B)) \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)))$
41		df-ltpq	$⊢ <_{𝑝𝑸} = \{⟨x, y⟩ \| ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) <_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)))\}$
42	1 2 21 40 41	brab	$⊢ ⟨A, B⟩ <_{𝑝𝑸} ⟨C, D⟩ \leftrightarrow ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B))$
43		simpr	$⊢ ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)) \to (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)$
44		ltrelpi	$⊢ <_{𝑵} \subseteq 𝑵 \times 𝑵$
45	44	brel	$⊢ (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B) \to (A \cdot_{𝑵} D \in 𝑵 \land C \cdot_{𝑵} B \in 𝑵)$
46		dmmulpi	$⊢ dom \cdot_{𝑵} = 𝑵 \times 𝑵$
47		0npi	$⊢ \neg \emptyset \in 𝑵$
48	46 47	ndmovrcl	$⊢ A \cdot_{𝑵} D \in 𝑵 \to (A \in 𝑵 \land D \in 𝑵)$
49	46 47	ndmovrcl	$⊢ C \cdot_{𝑵} B \in 𝑵 \to (C \in 𝑵 \land B \in 𝑵)$
50	48 49	anim12i	$⊢ (A \cdot_{𝑵} D \in 𝑵 \land C \cdot_{𝑵} B \in 𝑵) \to ((A \in 𝑵 \land D \in 𝑵) \land (C \in 𝑵 \land B \in 𝑵))$
51		opelxpi	$⊢ (A \in 𝑵 \land B \in 𝑵) \to ⟨A, B⟩ \in (𝑵 \times 𝑵)$
52	51	ad2ant2rl	$⊢ ((A \in 𝑵 \land D \in 𝑵) \land (C \in 𝑵 \land B \in 𝑵)) \to ⟨A, B⟩ \in (𝑵 \times 𝑵)$
53		simprl	$⊢ ((A \in 𝑵 \land D \in 𝑵) \land (C \in 𝑵 \land B \in 𝑵)) \to C \in 𝑵$
54		simplr	$⊢ ((A \in 𝑵 \land D \in 𝑵) \land (C \in 𝑵 \land B \in 𝑵)) \to D \in 𝑵$
55	53 54	opelxpd	$⊢ ((A \in 𝑵 \land D \in 𝑵) \land (C \in 𝑵 \land B \in 𝑵)) \to ⟨C, D⟩ \in (𝑵 \times 𝑵)$
56	52 55	jca	$⊢ ((A \in 𝑵 \land D \in 𝑵) \land (C \in 𝑵 \land B \in 𝑵)) \to (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))$
57	45 50 56	3syl	$⊢ (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B) \to (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵))$
58	57	ancri	$⊢ (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B) \to ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B))$
59	43 58	impbii	$⊢ ((⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \land (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)) \leftrightarrow (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)$
60	42 59	bitri	$⊢ ⟨A, B⟩ <_{𝑝𝑸} ⟨C, D⟩ \leftrightarrow (A \cdot_{𝑵} D) <_{𝑵} (C \cdot_{𝑵} B)$

Metamath Proof Explorer

Theorem ordpipq

Proof