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 syl6bi
 |-  ( ( 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
 |-