Metamath Proof Explorer


Theorem ltrnq

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

Ref Expression
Assertion ltrnq
|- ( A  ( *Q ` B ) 

Proof

Step Hyp Ref Expression
1 ltrelnq
 |-  
2 1 brel
 |-  ( A  ( A e. Q. /\ B e. Q. ) )
3 1 brel
 |-  ( ( *Q ` B )  ( ( *Q ` B ) e. Q. /\ ( *Q ` A ) e. Q. ) )
4 dmrecnq
 |-  dom *Q = Q.
5 0nnq
 |-  -. (/) e. Q.
6 4 5 ndmfvrcl
 |-  ( ( *Q ` B ) e. Q. -> B e. Q. )
7 4 5 ndmfvrcl
 |-  ( ( *Q ` A ) e. Q. -> A e. Q. )
8 6 7 anim12ci
 |-  ( ( ( *Q ` B ) e. Q. /\ ( *Q ` A ) e. Q. ) -> ( A e. Q. /\ B e. Q. ) )
9 3 8 syl
 |-  ( ( *Q ` B )  ( A e. Q. /\ B e. Q. ) )
10 breq1
 |-  ( x = A -> ( x  A 
11 fveq2
 |-  ( x = A -> ( *Q ` x ) = ( *Q ` A ) )
12 11 breq2d
 |-  ( x = A -> ( ( *Q ` y )  ( *Q ` y ) 
13 10 12 bibi12d
 |-  ( x = A -> ( ( x  ( *Q ` y )  ( A  ( *Q ` y ) 
14 breq2
 |-  ( y = B -> ( A  A 
15 fveq2
 |-  ( y = B -> ( *Q ` y ) = ( *Q ` B ) )
16 15 breq1d
 |-  ( y = B -> ( ( *Q ` y )  ( *Q ` B ) 
17 14 16 bibi12d
 |-  ( y = B -> ( ( A  ( *Q ` y )  ( A  ( *Q ` B ) 
18 recclnq
 |-  ( x e. Q. -> ( *Q ` x ) e. Q. )
19 recclnq
 |-  ( y e. Q. -> ( *Q ` y ) e. Q. )
20 mulclnq
 |-  ( ( ( *Q ` x ) e. Q. /\ ( *Q ` y ) e. Q. ) -> ( ( *Q ` x ) .Q ( *Q ` y ) ) e. Q. )
21 18 19 20 syl2an
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( *Q ` x ) .Q ( *Q ` y ) ) e. Q. )
22 ltmnq
 |-  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) e. Q. -> ( x  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) 
23 21 22 syl
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) 
24 mulcomnq
 |-  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) = ( x .Q ( ( *Q ` x ) .Q ( *Q ` y ) ) )
25 mulassnq
 |-  ( ( x .Q ( *Q ` x ) ) .Q ( *Q ` y ) ) = ( x .Q ( ( *Q ` x ) .Q ( *Q ` y ) ) )
26 mulcomnq
 |-  ( ( x .Q ( *Q ` x ) ) .Q ( *Q ` y ) ) = ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) )
27 24 25 26 3eqtr2i
 |-  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) = ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) )
28 recidnq
 |-  ( x e. Q. -> ( x .Q ( *Q ` x ) ) = 1Q )
29 28 oveq2d
 |-  ( x e. Q. -> ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) ) = ( ( *Q ` y ) .Q 1Q ) )
30 mulidnq
 |-  ( ( *Q ` y ) e. Q. -> ( ( *Q ` y ) .Q 1Q ) = ( *Q ` y ) )
31 19 30 syl
 |-  ( y e. Q. -> ( ( *Q ` y ) .Q 1Q ) = ( *Q ` y ) )
32 29 31 sylan9eq
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) ) = ( *Q ` y ) )
33 27 32 eqtrid
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) = ( *Q ` y ) )
34 mulassnq
 |-  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q y ) = ( ( *Q ` x ) .Q ( ( *Q ` y ) .Q y ) )
35 mulcomnq
 |-  ( ( *Q ` y ) .Q y ) = ( y .Q ( *Q ` y ) )
36 35 oveq2i
 |-  ( ( *Q ` x ) .Q ( ( *Q ` y ) .Q y ) ) = ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) )
37 34 36 eqtri
 |-  ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q y ) = ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) )
38 recidnq
 |-  ( y e. Q. -> ( y .Q ( *Q ` y ) ) = 1Q )
39 38 oveq2d
 |-  ( y e. Q. -> ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) ) = ( ( *Q ` x ) .Q 1Q ) )
40 mulidnq
 |-  ( ( *Q ` x ) e. Q. -> ( ( *Q ` x ) .Q 1Q ) = ( *Q ` x ) )
41 18 40 syl
 |-  ( x e. Q. -> ( ( *Q ` x ) .Q 1Q ) = ( *Q ` x ) )
42 39 41 sylan9eqr
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) ) = ( *Q ` x ) )
43 37 42 eqtrid
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q y ) = ( *Q ` x ) )
44 33 43 breq12d
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x )  ( *Q ` y ) 
45 23 44 bitrd
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x  ( *Q ` y ) 
46 13 17 45 vtocl2ga
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  ( *Q ` B ) 
47 2 9 46 pm5.21nii
 |-  ( A  ( *Q ` B )