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 syl5eq 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 )