Metamath Proof Explorer


Theorem ltanq

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

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

Proof

Step Hyp Ref Expression
1 addnqf
 |-  +Q : ( Q. X. Q. ) --> Q.
2 1 fdmi
 |-  dom +Q = ( Q. X. Q. )
3 ltrelnq
 |-  
4 0nnq
 |-  -. (/) e. Q.
5 ordpinq
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) ) 
6 5 3adant3
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) ) 
7 elpqn
 |-  ( C e. Q. -> C e. ( N. X. N. ) )
8 7 3ad2ant3
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C e. ( N. X. N. ) )
9 elpqn
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
10 9 3ad2ant1
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A e. ( N. X. N. ) )
11 addpipq2
 |-  ( ( C e. ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> ( C +pQ A ) = <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. )
12 8 10 11 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +pQ A ) = <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. )
13 elpqn
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
14 13 3ad2ant2
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> B e. ( N. X. N. ) )
15 addpipq2
 |-  ( ( C e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( C +pQ B ) = <. ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` B ) ) >. )
16 8 14 15 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +pQ B ) = <. ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` B ) ) >. )
17 12 16 breq12d
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C +pQ A )  <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . ) )
18 addpqnq
 |-  ( ( C e. Q. /\ A e. Q. ) -> ( C +Q A ) = ( /Q ` ( C +pQ A ) ) )
19 18 ancoms
 |-  ( ( A e. Q. /\ C e. Q. ) -> ( C +Q A ) = ( /Q ` ( C +pQ A ) ) )
20 19 3adant2
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +Q A ) = ( /Q ` ( C +pQ A ) ) )
21 addpqnq
 |-  ( ( C e. Q. /\ B e. Q. ) -> ( C +Q B ) = ( /Q ` ( C +pQ B ) ) )
22 21 ancoms
 |-  ( ( B e. Q. /\ C e. Q. ) -> ( C +Q B ) = ( /Q ` ( C +pQ B ) ) )
23 22 3adant1
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +Q B ) = ( /Q ` ( C +pQ B ) ) )
24 20 23 breq12d
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C +Q A )  ( /Q ` ( C +pQ A ) ) 
25 lterpq
 |-  ( ( C +pQ A )  ( /Q ` ( C +pQ A ) ) 
26 24 25 bitr4di
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C +Q A )  ( C +pQ A ) 
27 xp2nd
 |-  ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. )
28 8 27 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` C ) e. N. )
29 mulclpi
 |-  ( ( ( 2nd ` C ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. )
30 28 28 29 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. )
31 ltmpi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) 
32 30 31 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) 
33 xp2nd
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
34 14 33 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` B ) e. N. )
35 mulclpi
 |-  ( ( ( 2nd ` C ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 2nd ` C ) .N ( 2nd ` B ) ) e. N. )
36 28 34 35 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` C ) .N ( 2nd ` B ) ) e. N. )
37 xp1st
 |-  ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. )
38 8 37 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` C ) e. N. )
39 xp2nd
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
40 10 39 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` A ) e. N. )
41 mulclpi
 |-  ( ( ( 1st ` C ) e. N. /\ ( 2nd ` A ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. )
42 38 40 41 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. )
43 mulclpi
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) e. N. /\ ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. ) -> ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. )
44 36 42 43 syl2anc
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. )
45 ltapi
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) )  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) 
46 44 45 syl
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) )  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) 
47 32 46 bitrd
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) 
48 mulcompi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) )
49 fvex
 |-  ( 1st ` A ) e. _V
50 fvex
 |-  ( 2nd ` B ) e. _V
51 fvex
 |-  ( 2nd ` C ) e. _V
52 mulcompi
 |-  ( x .N y ) = ( y .N x )
53 mulasspi
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
54 49 50 51 52 53 51 caov411
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) )
55 48 54 eqtri
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) )
56 55 oveq2i
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) )
57 distrpi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) )
58 mulcompi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) )
59 56 57 58 3eqtr2i
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) )
60 mulcompi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) )
61 fvex
 |-  ( 1st ` C ) e. _V
62 fvex
 |-  ( 2nd ` A ) e. _V
63 61 62 51 52 53 50 caov411
 |-  ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) )
64 60 63 eqtri
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) )
65 mulcompi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) )
66 fvex
 |-  ( 1st ` B ) e. _V
67 66 62 51 52 53 51 caov411
 |-  ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
68 65 67 eqtri
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) )
69 64 68 oveq12i
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) )
70 distrpi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) )
71 mulcompi
 |-  ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` A ) ) )
72 69 70 71 3eqtr2i
 |-  ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` A ) ) )
73 59 72 breq12i
 |-  ( ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) )  ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) 
74 47 73 bitrdi
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) 
75 ordpipq
 |-  ( <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . <-> ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) 
76 74 75 bitr4di
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . ) )
77 17 26 76 3bitr4rd
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( C +Q A ) 
78 6 77 bitrd
 |-  ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A  ( C +Q A ) 
79 2 3 4 78 ndmovord
 |-  ( C e. Q. -> ( A  ( C +Q A )