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 )