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 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A
6 5 3adant3 A 𝑸 B 𝑸 C 𝑸 A < 𝑸 B 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd 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 = 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 2 nd C 𝑵 2 nd A
12 8 10 11 syl2anc A 𝑸 B 𝑸 C 𝑸 C + 𝑝𝑸 A = 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 2 nd C 𝑵 2 nd A
13 elpqn B 𝑸 B 𝑵 × 𝑵
14 13 3ad2ant2 A 𝑸 B 𝑸 C 𝑸 B 𝑵 × 𝑵
15 addpipq2 C 𝑵 × 𝑵 B 𝑵 × 𝑵 C + 𝑝𝑸 B = 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 2 nd C 𝑵 2 nd B
16 8 14 15 syl2anc A 𝑸 B 𝑸 C 𝑸 C + 𝑝𝑸 B = 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 2 nd C 𝑵 2 nd B
17 12 16 breq12d A 𝑸 B 𝑸 C 𝑸 C + 𝑝𝑸 A < 𝑝𝑸 C + 𝑝𝑸 B 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 2 nd C 𝑵 2 nd A < 𝑝𝑸 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 2 nd C 𝑵 2 nd 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 𝑵 × 𝑵 2 nd C 𝑵
28 8 27 syl A 𝑸 B 𝑸 C 𝑸 2 nd C 𝑵
29 mulclpi 2 nd C 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd C 𝑵
30 28 28 29 syl2anc A 𝑸 B 𝑸 C 𝑸 2 nd C 𝑵 2 nd C 𝑵
31 ltmpi 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A
32 30 31 syl A 𝑸 B 𝑸 C 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A
33 xp2nd B 𝑵 × 𝑵 2 nd B 𝑵
34 14 33 syl A 𝑸 B 𝑸 C 𝑸 2 nd B 𝑵
35 mulclpi 2 nd C 𝑵 2 nd B 𝑵 2 nd C 𝑵 2 nd B 𝑵
36 28 34 35 syl2anc A 𝑸 B 𝑸 C 𝑸 2 nd C 𝑵 2 nd B 𝑵
37 xp1st C 𝑵 × 𝑵 1 st C 𝑵
38 8 37 syl A 𝑸 B 𝑸 C 𝑸 1 st C 𝑵
39 xp2nd A 𝑵 × 𝑵 2 nd A 𝑵
40 10 39 syl A 𝑸 B 𝑸 C 𝑸 2 nd A 𝑵
41 mulclpi 1 st C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd A 𝑵
42 38 40 41 syl2anc A 𝑸 B 𝑸 C 𝑸 1 st C 𝑵 2 nd A 𝑵
43 mulclpi 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A 𝑵
44 36 42 43 syl2anc A 𝑸 B 𝑸 C 𝑸 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A 𝑵
45 ltapi 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A
46 44 45 syl A 𝑸 B 𝑸 C 𝑸 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A
47 32 46 bitrd A 𝑸 B 𝑸 C 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A
48 mulcompi 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B = 1 st A 𝑵 2 nd B 𝑵 2 nd C 𝑵 2 nd C
49 fvex 1 st A V
50 fvex 2 nd B V
51 fvex 2 nd C V
52 mulcompi x 𝑵 y = y 𝑵 x
53 mulasspi x 𝑵 y 𝑵 z = x 𝑵 y 𝑵 z
54 49 50 51 52 53 51 caov411 1 st A 𝑵 2 nd B 𝑵 2 nd C 𝑵 2 nd C = 2 nd C 𝑵 2 nd B 𝑵 1 st A 𝑵 2 nd C
55 48 54 eqtri 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B = 2 nd C 𝑵 2 nd B 𝑵 1 st A 𝑵 2 nd C
56 55 oveq2i 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B = 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st A 𝑵 2 nd C
57 distrpi 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C = 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st A 𝑵 2 nd C
58 mulcompi 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C = 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd B
59 56 57 58 3eqtr2i 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B = 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd B
60 mulcompi 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A = 1 st C 𝑵 2 nd A 𝑵 2 nd C 𝑵 2 nd B
61 fvex 1 st C V
62 fvex 2 nd A V
63 61 62 51 52 53 50 caov411 1 st C 𝑵 2 nd A 𝑵 2 nd C 𝑵 2 nd B = 2 nd C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd B
64 60 63 eqtri 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A = 2 nd C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd B
65 mulcompi 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A = 1 st B 𝑵 2 nd A 𝑵 2 nd C 𝑵 2 nd C
66 fvex 1 st B V
67 66 62 51 52 53 51 caov411 1 st B 𝑵 2 nd A 𝑵 2 nd C 𝑵 2 nd C = 2 nd C 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd C
68 65 67 eqtri 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A = 2 nd C 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd C
69 64 68 oveq12i 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A = 2 nd C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd B + 𝑵 2 nd C 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd C
70 distrpi 2 nd C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C = 2 nd C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd B + 𝑵 2 nd C 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd C
71 mulcompi 2 nd C 𝑵 2 nd A 𝑵 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C = 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd A
72 69 70 71 3eqtr2i 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A = 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd A
73 59 72 breq12i 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st A 𝑵 2 nd B < 𝑵 2 nd C 𝑵 2 nd B 𝑵 1 st C 𝑵 2 nd A + 𝑵 2 nd C 𝑵 2 nd C 𝑵 1 st B 𝑵 2 nd A 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd B < 𝑵 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd A
74 47 73 bitrdi A 𝑸 B 𝑸 C 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd B < 𝑵 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd A
75 ordpipq 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 2 nd C 𝑵 2 nd A < 𝑝𝑸 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 2 nd C 𝑵 2 nd B 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd B < 𝑵 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 𝑵 2 nd C 𝑵 2 nd A
76 74 75 bitr4di A 𝑸 B 𝑸 C 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A 1 st C 𝑵 2 nd A + 𝑵 1 st A 𝑵 2 nd C 2 nd C 𝑵 2 nd A < 𝑝𝑸 1 st C 𝑵 2 nd B + 𝑵 1 st B 𝑵 2 nd C 2 nd C 𝑵 2 nd B
77 17 26 76 3bitr4rd A 𝑸 B 𝑸 C 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd 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