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∈𝑸→A<𝑸B↔C+𝑸A<𝑸C+𝑸B

Proof

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