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 )