Metamath Proof Explorer


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
|- ( <. A , B >. . <-> ( A .N D ) 

Proof

Step Hyp Ref Expression
1 opex
 |-  <. A , B >. e. _V
2 opex
 |-  <. C , D >. e. _V
3 eleq1
 |-  ( x = <. A , B >. -> ( x e. ( N. X. N. ) <-> <. A , B >. e. ( N. X. N. ) ) )
4 3 anbi1d
 |-  ( x = <. A , B >. -> ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) <-> ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) )
5 4 anbi1d
 |-  ( x = <. A , B >. -> ( ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )  ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) 
6 fveq2
 |-  ( x = <. A , B >. -> ( 1st ` x ) = ( 1st ` <. A , B >. ) )
7 opelxp
 |-  ( <. A , B >. e. ( N. X. N. ) <-> ( A e. N. /\ B e. N. ) )
8 op1stg
 |-  ( ( A e. N. /\ B e. N. ) -> ( 1st ` <. A , B >. ) = A )
9 7 8 sylbi
 |-  ( <. A , B >. e. ( N. X. N. ) -> ( 1st ` <. A , B >. ) = A )
10 9 adantr
 |-  ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( 1st ` <. A , B >. ) = A )
11 6 10 sylan9eq
 |-  ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( 1st ` x ) = A )
12 11 oveq1d
 |-  ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( A .N ( 2nd ` y ) ) )
13 fveq2
 |-  ( x = <. A , B >. -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) )
14 op2ndg
 |-  ( ( A e. N. /\ B e. N. ) -> ( 2nd ` <. A , B >. ) = B )
15 7 14 sylbi
 |-  ( <. A , B >. e. ( N. X. N. ) -> ( 2nd ` <. A , B >. ) = B )
16 15 adantr
 |-  ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( 2nd ` <. A , B >. ) = B )
17 13 16 sylan9eq
 |-  ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( 2nd ` x ) = B )
18 17 oveq2d
 |-  ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) = ( ( 1st ` y ) .N B ) )
19 12 18 breq12d
 |-  ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) )  ( A .N ( 2nd ` y ) ) 
20 19 pm5.32da
 |-  ( x = <. A , B >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )  ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) 
21 5 20 bitrd
 |-  ( x = <. A , B >. -> ( ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) )  ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) 
22 eleq1
 |-  ( y = <. C , D >. -> ( y e. ( N. X. N. ) <-> <. C , D >. e. ( N. X. N. ) ) )
23 22 anbi2d
 |-  ( y = <. C , D >. -> ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) <-> ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) )
24 23 anbi1d
 |-  ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) )  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) 
25 fveq2
 |-  ( y = <. C , D >. -> ( 2nd ` y ) = ( 2nd ` <. C , D >. ) )
26 opelxp
 |-  ( <. C , D >. e. ( N. X. N. ) <-> ( C e. N. /\ D e. N. ) )
27 op2ndg
 |-  ( ( C e. N. /\ D e. N. ) -> ( 2nd ` <. C , D >. ) = D )
28 26 27 sylbi
 |-  ( <. C , D >. e. ( N. X. N. ) -> ( 2nd ` <. C , D >. ) = D )
29 28 adantl
 |-  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) -> ( 2nd ` <. C , D >. ) = D )
30 25 29 sylan9eq
 |-  ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( 2nd ` y ) = D )
31 30 oveq2d
 |-  ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( A .N ( 2nd ` y ) ) = ( A .N D ) )
32 fveq2
 |-  ( y = <. C , D >. -> ( 1st ` y ) = ( 1st ` <. C , D >. ) )
33 op1stg
 |-  ( ( C e. N. /\ D e. N. ) -> ( 1st ` <. C , D >. ) = C )
34 26 33 sylbi
 |-  ( <. C , D >. e. ( N. X. N. ) -> ( 1st ` <. C , D >. ) = C )
35 34 adantl
 |-  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) -> ( 1st ` <. C , D >. ) = C )
36 32 35 sylan9eq
 |-  ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( 1st ` y ) = C )
37 36 oveq1d
 |-  ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( ( 1st ` y ) .N B ) = ( C .N B ) )
38 31 37 breq12d
 |-  ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( ( A .N ( 2nd ` y ) )  ( A .N D ) 
39 38 pm5.32da
 |-  ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) )  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) 
40 24 39 bitrd
 |-  ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) )  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) 
41 df-ltpq
 |-  . | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) 
42 1 2 21 40 41 brab
 |-  ( <. A , B >. . <-> ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) 
43 simpr
 |-  ( ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D )  ( A .N D ) 
44 ltrelpi
 |-  
45 44 brel
 |-  ( ( A .N D )  ( ( A .N D ) e. N. /\ ( C .N B ) e. N. ) )
46 dmmulpi
 |-  dom .N = ( N. X. N. )
47 0npi
 |-  -. (/) e. N.
48 46 47 ndmovrcl
 |-  ( ( A .N D ) e. N. -> ( A e. N. /\ D e. N. ) )
49 46 47 ndmovrcl
 |-  ( ( C .N B ) e. N. -> ( C e. N. /\ B e. N. ) )
50 48 49 anim12i
 |-  ( ( ( A .N D ) e. N. /\ ( C .N B ) e. N. ) -> ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) )
51 opelxpi
 |-  ( ( A e. N. /\ B e. N. ) -> <. A , B >. e. ( N. X. N. ) )
52 51 ad2ant2rl
 |-  ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> <. A , B >. e. ( N. X. N. ) )
53 simprl
 |-  ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> C e. N. )
54 simplr
 |-  ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> D e. N. )
55 53 54 opelxpd
 |-  ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> <. C , D >. e. ( N. X. N. ) )
56 52 55 jca
 |-  ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) )
57 45 50 56 3syl
 |-  ( ( A .N D )  ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) )
58 57 ancri
 |-  ( ( A .N D )  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) 
59 43 58 impbii
 |-  ( ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D )  ( A .N D ) 
60 42 59 bitri
 |-  ( <. A , B >. . <-> ( A .N D )