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