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 syl6bb 
 |-  ( ( 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 syl6bbr 
 |-  ( ( 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 syl6bbr 
 |-  ( ( 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 )