Metamath Proof Explorer

Theorem ltsonq

Description: 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996) (Revised by Mario Carneiro, 4-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltsonq 
|-

Proof

Step Hyp Ref Expression
1 elpqn 
 |-  ( x e. Q. -> x e. ( N. X. N. ) )
2 1 adantr 
 |-  ( ( x e. Q. /\ y e. Q. ) -> x e. ( N. X. N. ) )
3 xp1st 
 |-  ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
4 2 3 syl 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( 1st ` x ) e. N. )
5 elpqn 
 |-  ( y e. Q. -> y e. ( N. X. N. ) )
6 5 adantl 
 |-  ( ( x e. Q. /\ y e. Q. ) -> y e. ( N. X. N. ) )
7 xp2nd 
 |-  ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
8 6 7 syl 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( 2nd ` y ) e. N. )
9 mulclpi 
 |-  ( ( ( 1st ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. )
10 4 8 9 syl2anc 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. )
11 xp1st 
 |-  ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
12 6 11 syl 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( 1st ` y ) e. N. )
13 xp2nd 
 |-  ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
14 2 13 syl 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( 2nd ` x ) e. N. )
15 mulclpi 
 |-  ( ( ( 1st ` y ) e. N. /\ ( 2nd ` x ) e. N. ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. )
16 12 14 15 syl2anc 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. )
17 ltsopi 
 |-
18 sotric 
 |-  ( (  ( ( ( 1st ` x ) .N ( 2nd ` y ) )  -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) )
19 17 18 mpan 
 |-  ( ( ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. /\ ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) )  -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) )
20 10 16 19 syl2anc 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) )  -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) )
21 ordpinq 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x  ( ( 1st ` x ) .N ( 2nd ` y ) )
22 fveq2 
 |-  ( x = y -> ( 1st ` x ) = ( 1st ` y ) )
23 fveq2 
 |-  ( x = y -> ( 2nd ` x ) = ( 2nd ` y ) )
24 23 eqcomd 
 |-  ( x = y -> ( 2nd ` y ) = ( 2nd ` x ) )
25 22 24 oveq12d 
 |-  ( x = y -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) )
26 enqbreq2 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) )
27 1 5 26 syl2an 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) )
28 enqeq 
 |-  ( ( x e. Q. /\ y e. Q. /\ x ~Q y ) -> x = y )
29 28 3expia 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> x = y ) )
30 27 29 sylbird 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) -> x = y ) )
31 25 30 impbid2 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x = y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) )
32 ordpinq 
 |-  ( ( y e. Q. /\ x e. Q. ) -> ( y  ( ( 1st ` y ) .N ( 2nd ` x ) )
33 32 ancoms 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( y  ( ( 1st ` y ) .N ( 2nd ` x ) )
34 31 33 orbi12d 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( x = y \/ y  ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) )
35 34 notbid 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( -. ( x = y \/ y  -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) )
36 20 21 35 3bitr4d 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x  -. ( x = y \/ y
37 21 3adant3 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x  ( ( 1st ` x ) .N ( 2nd ` y ) )
38 elpqn 
 |-  ( z e. Q. -> z e. ( N. X. N. ) )
39 38 3ad2ant3 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> z e. ( N. X. N. ) )
40 xp2nd 
 |-  ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. )
41 ltmpi 
 |-  ( ( 2nd ` z ) e. N. -> ( ( ( 1st ` x ) .N ( 2nd ` y ) )  ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )
42 39 40 41 3syl 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) )  ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )
43 37 42 bitrd 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x  ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )
44 ordpinq 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y  ( ( 1st ` y ) .N ( 2nd ` z ) )
45 44 3adant1 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( y  ( ( 1st ` y ) .N ( 2nd ` z ) )
46 1 3ad2ant1 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> x e. ( N. X. N. ) )
47 ltmpi 
 |-  ( ( 2nd ` x ) e. N. -> ( ( ( 1st ` y ) .N ( 2nd ` z ) )  ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) )
48 46 13 47 3syl 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( ( 1st ` y ) .N ( 2nd ` z ) )  ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) )
49 45 48 bitrd 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( y  ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) )
50 43 49 anbi12d 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( x  ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )
51 fvex 
 |-  ( 2nd ` x ) e. _V
52 fvex 
 |-  ( 1st ` y ) e. _V
53 fvex 
 |-  ( 2nd ` z ) e. _V
54 mulcompi 
 |-  ( r .N s ) = ( s .N r )
55 mulasspi 
 |-  ( ( r .N s ) .N t ) = ( r .N ( s .N t ) )
56 51 52 53 54 55 caov13 
 |-  ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) ) = ( ( 2nd ` z ) .N ( ( 1st ` y ) .N ( 2nd ` x ) ) )
57 fvex 
 |-  ( 1st ` z ) e. _V
58 fvex 
 |-  ( 2nd ` y ) e. _V
59 51 57 58 54 55 caov13 
 |-  ( ( 2nd ` x ) .N ( ( 1st ` z ) .N ( 2nd ` y ) ) ) = ( ( 2nd ` y ) .N ( ( 1st ` z ) .N ( 2nd ` x ) ) )
60 56 59 breq12i 
 |-  ( ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) )  ( ( 2nd ` z ) .N ( ( 1st ` y ) .N ( 2nd ` x ) ) )
61 fvex 
 |-  ( 1st ` x ) e. _V
62 53 61 58 54 55 caov13 
 |-  ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) = ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
63 ltrelpi 
 |-
64 17 63 sotri 
 |-  ( ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )  ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )
65 62 64 eqbrtrrid 
 |-  ( ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )  ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
66 60 65 sylan2b 
 |-  ( ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) )  ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
67 50 66 biimtrdi 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( x  ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
68 ordpinq 
 |-  ( ( x e. Q. /\ z e. Q. ) -> ( x  ( ( 1st ` x ) .N ( 2nd ` z ) )
69 68 3adant2 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x  ( ( 1st ` x ) .N ( 2nd ` z ) )
70 5 3ad2ant2 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> y e. ( N. X. N. ) )
71 ltmpi 
 |-  ( ( 2nd ` y ) e. N. -> ( ( ( 1st ` x ) .N ( 2nd ` z ) )  ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
72 70 7 71 3syl 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` z ) )  ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
73 69 72 bitrd 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x  ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) )
74 67 73 sylibrd 
 |-  ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( x  x
75 36 74 isso2i 
 |-