This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 ‘ 𝐴 ) ) ) )