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	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <Q 𝐵 ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		brinxp	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <pQ 𝐵 ↔ 𝐴 ( <pQ ∩ ( Q × Q ) ) 𝐵 ) )
2		df-ltnq	⊢ <Q = ( <pQ ∩ ( Q × Q ) )
3	2	breqi	⊢ ( 𝐴 <Q 𝐵 ↔ 𝐴 ( <pQ ∩ ( Q × Q ) ) 𝐵 )
4	1 3	bitr4di	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <pQ 𝐵 ↔ 𝐴 <Q 𝐵 ) )
5		relxp	⊢ Rel ( N × N )
6		elpqn	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
7		1st2nd	⊢ ( ( Rel ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
8	5 6 7	sylancr	⊢ ( 𝐴 ∈ Q → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
9		elpqn	⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
10		1st2nd	⊢ ( ( Rel ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → 𝐵 = ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ )
11	5 9 10	sylancr	⊢ ( 𝐵 ∈ Q → 𝐵 = ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ )
12	8 11	breqan12d	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <pQ 𝐵 ↔ ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ <pQ ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ ) )
13		ordpipq	⊢ ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ <pQ ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) )
14	12 13	bitrdi	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <pQ 𝐵 ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
15	4 14	bitr3d	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <Q 𝐵 ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )