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 e. Q. /\ B e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) )

Proof

Step Hyp Ref Expression
1 brinxp 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  A (
2 df-ltnq 
 |-
3 2 breqi 
 |-  ( A  A (
4 1 3 bitr4di 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  A
5 relxp 
 |-  Rel ( N. X. N. )
6 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
7 1st2nd 
 |-  ( ( Rel ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
8 5 6 7 sylancr 
 |-  ( A e. Q. -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
9 elpqn 
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
10 1st2nd 
 |-  ( ( Rel ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
11 5 9 10 sylancr 
 |-  ( B e. Q. -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
12 8 11 breqan12d 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  <. ( 1st ` A ) , ( 2nd ` A ) >. . ) )
13 ordpipq 
 |-  ( <. ( 1st ` A ) , ( 2nd ` A ) >. . <-> ( ( 1st ` A ) .N ( 2nd ` B ) )
14 12 13 bitrdi 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) )
15 4 14 bitr3d 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) )