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