Metamath Proof Explorer


Theorem ltmnq

Description: Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of Gleason p. 120. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltmnq
|- ( C e. Q. -> ( A  ( C .Q A ) 

Proof

Step Hyp Ref Expression
1 mulnqf
 |-  .Q : ( Q. X. Q. ) --> Q.
2 1 fdmi
 |-  dom .Q = ( Q. X. Q. )
3 ltrelnq
 |-  
4 0nnq
 |-  -. (/) e. Q.
5 elpqn
 |-  ( C e. Q. -> C e. ( N. X. N. ) )
6 5 3ad2ant3
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C e. ( N. X. N. ) )
7 xp1st
 |-  ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. )
8 6 7 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` C ) e. N. )
9 xp2nd
 |-  ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. )
10 6 9 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` C ) e. N. )
11 mulclpi
 |-  ( ( ( 1st ` C ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` C ) ) e. N. )
12 8 10 11 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` C ) .N ( 2nd ` C ) ) e. N. )
13 ltmpi
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) e. N. -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) 
14 12 13 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) 
15 fvex
 |-  ( 1st ` C ) e. _V
16 fvex
 |-  ( 2nd ` C ) e. _V
17 fvex
 |-  ( 1st ` A ) e. _V
18 mulcompi
 |-  ( x .N y ) = ( y .N x )
19 mulasspi
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
20 fvex
 |-  ( 2nd ` B ) e. _V
21 15 16 17 18 19 20 caov4
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` C ) .N ( 1st ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) )
22 fvex
 |-  ( 1st ` B ) e. _V
23 fvex
 |-  ( 2nd ` A ) e. _V
24 15 16 22 18 19 23 caov4
 |-  ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` C ) .N ( 1st ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` A ) ) )
25 21 24 breq12i
 |-  ( ( ( ( 1st ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) )  ( ( ( 1st ` C ) .N ( 1st ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) 
26 14 25 bitrdi
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 1st ` C ) .N ( 1st ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) 
27 ordpipq
 |-  ( <. ( ( 1st ` C ) .N ( 1st ` A ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . <-> ( ( ( 1st ` C ) .N ( 1st ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) 
28 26 27 bitr4di
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  <. ( ( 1st ` C ) .N ( 1st ` A ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . ) )
29 elpqn
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
30 29 3ad2ant1
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A e. ( N. X. N. ) )
31 mulpipq2
 |-  ( ( C e. ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> ( C .pQ A ) = <. ( ( 1st ` C ) .N ( 1st ` A ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. )
32 6 30 31 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C .pQ A ) = <. ( ( 1st ` C ) .N ( 1st ` A ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. )
33 elpqn
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
34 33 3ad2ant2
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> B e. ( N. X. N. ) )
35 mulpipq2
 |-  ( ( C e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( C .pQ B ) = <. ( ( 1st ` C ) .N ( 1st ` B ) ) , ( ( 2nd ` C ) .N ( 2nd ` B ) ) >. )
36 6 34 35 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C .pQ B ) = <. ( ( 1st ` C ) .N ( 1st ` B ) ) , ( ( 2nd ` C ) .N ( 2nd ` B ) ) >. )
37 32 36 breq12d
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C .pQ A )  <. ( ( 1st ` C ) .N ( 1st ` A ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . ) )
38 28 37 bitr4d
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( C .pQ A ) 
39 ordpinq
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) ) 
40 39 3adant3
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) ) 
41 mulpqnq
 |-  ( ( C e. Q. /\ A e. Q. ) -> ( C .Q A ) = ( /Q ` ( C .pQ A ) ) )
42 41 ancoms
 |-  ( ( A e. Q. /\ C e. Q. ) -> ( C .Q A ) = ( /Q ` ( C .pQ A ) ) )
43 42 3adant2
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C .Q A ) = ( /Q ` ( C .pQ A ) ) )
44 mulpqnq
 |-  ( ( C e. Q. /\ B e. Q. ) -> ( C .Q B ) = ( /Q ` ( C .pQ B ) ) )
45 44 ancoms
 |-  ( ( B e. Q. /\ C e. Q. ) -> ( C .Q B ) = ( /Q ` ( C .pQ B ) ) )
46 45 3adant1
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C .Q B ) = ( /Q ` ( C .pQ B ) ) )
47 43 46 breq12d
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C .Q A )  ( /Q ` ( C .pQ A ) ) 
48 lterpq
 |-  ( ( C .pQ A )  ( /Q ` ( C .pQ A ) ) 
49 47 48 bitr4di
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C .Q A )  ( C .pQ A ) 
50 38 40 49 3bitr4d
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A  ( C .Q A ) 
51 2 3 4 50 ndmovord
 |-  ( C e. Q. -> ( A  ( C .Q A )