Metamath Proof Explorer


Theorem ltexnq

Description: Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of Gleason p. 119. (Contributed by NM, 24-Apr-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltexnq B 𝑸 A < 𝑸 B x A + 𝑸 x = B

Proof

Step Hyp Ref Expression
1 ltrelnq < 𝑸 𝑸 × 𝑸
2 1 brel A < 𝑸 B A 𝑸 B 𝑸
3 ordpinq A 𝑸 B 𝑸 A < 𝑸 B 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A
4 elpqn A 𝑸 A 𝑵 × 𝑵
5 4 adantr A 𝑸 B 𝑸 A 𝑵 × 𝑵
6 xp1st A 𝑵 × 𝑵 1 st A 𝑵
7 5 6 syl A 𝑸 B 𝑸 1 st A 𝑵
8 elpqn B 𝑸 B 𝑵 × 𝑵
9 8 adantl A 𝑸 B 𝑸 B 𝑵 × 𝑵
10 xp2nd B 𝑵 × 𝑵 2 nd B 𝑵
11 9 10 syl A 𝑸 B 𝑸 2 nd B 𝑵
12 mulclpi 1 st A 𝑵 2 nd B 𝑵 1 st A 𝑵 2 nd B 𝑵
13 7 11 12 syl2anc A 𝑸 B 𝑸 1 st A 𝑵 2 nd B 𝑵
14 xp1st B 𝑵 × 𝑵 1 st B 𝑵
15 9 14 syl A 𝑸 B 𝑸 1 st B 𝑵
16 xp2nd A 𝑵 × 𝑵 2 nd A 𝑵
17 5 16 syl A 𝑸 B 𝑸 2 nd A 𝑵
18 mulclpi 1 st B 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd A 𝑵
19 15 17 18 syl2anc A 𝑸 B 𝑸 1 st B 𝑵 2 nd A 𝑵
20 ltexpi 1 st A 𝑵 2 nd B 𝑵 1 st B 𝑵 2 nd A 𝑵 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A y 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A
21 13 19 20 syl2anc A 𝑸 B 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A y 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A
22 relxp Rel 𝑵 × 𝑵
23 4 ad2antrr A 𝑸 B 𝑸 y 𝑵 A 𝑵 × 𝑵
24 1st2nd Rel 𝑵 × 𝑵 A 𝑵 × 𝑵 A = 1 st A 2 nd A
25 22 23 24 sylancr A 𝑸 B 𝑸 y 𝑵 A = 1 st A 2 nd A
26 25 oveq1d A 𝑸 B 𝑸 y 𝑵 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 1 st A 2 nd A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B
27 7 adantr A 𝑸 B 𝑸 y 𝑵 1 st A 𝑵
28 17 adantr A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵
29 simpr A 𝑸 B 𝑸 y 𝑵 y 𝑵
30 mulclpi 2 nd A 𝑵 2 nd B 𝑵 2 nd A 𝑵 2 nd B 𝑵
31 17 11 30 syl2anc A 𝑸 B 𝑸 2 nd A 𝑵 2 nd B 𝑵
32 31 adantr A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd B 𝑵
33 addpipq 1 st A 𝑵 2 nd A 𝑵 y 𝑵 2 nd A 𝑵 2 nd B 𝑵 1 st A 2 nd A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A 2 nd A 𝑵 2 nd A 𝑵 2 nd B
34 27 28 29 32 33 syl22anc A 𝑸 B 𝑸 y 𝑵 1 st A 2 nd A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A 2 nd A 𝑵 2 nd A 𝑵 2 nd B
35 26 34 eqtrd A 𝑸 B 𝑸 y 𝑵 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A 2 nd A 𝑵 2 nd A 𝑵 2 nd B
36 oveq2 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A 2 nd A 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 2 nd A 𝑵 1 st B 𝑵 2 nd A
37 distrpi 2 nd A 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 2 nd A 𝑵 1 st A 𝑵 2 nd B + 𝑵 2 nd A 𝑵 y
38 fvex 2 nd A V
39 fvex 1 st A V
40 fvex 2 nd B V
41 mulcompi x 𝑵 y = y 𝑵 x
42 mulasspi x 𝑵 y 𝑵 z = x 𝑵 y 𝑵 z
43 38 39 40 41 42 caov12 2 nd A 𝑵 1 st A 𝑵 2 nd B = 1 st A 𝑵 2 nd A 𝑵 2 nd B
44 mulcompi 2 nd A 𝑵 y = y 𝑵 2 nd A
45 43 44 oveq12i 2 nd A 𝑵 1 st A 𝑵 2 nd B + 𝑵 2 nd A 𝑵 y = 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A
46 37 45 eqtr2i 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A = 2 nd A 𝑵 1 st A 𝑵 2 nd B + 𝑵 y
47 mulasspi 2 nd A 𝑵 2 nd A 𝑵 1 st B = 2 nd A 𝑵 2 nd A 𝑵 1 st B
48 mulcompi 2 nd A 𝑵 1 st B = 1 st B 𝑵 2 nd A
49 48 oveq2i 2 nd A 𝑵 2 nd A 𝑵 1 st B = 2 nd A 𝑵 1 st B 𝑵 2 nd A
50 47 49 eqtri 2 nd A 𝑵 2 nd A 𝑵 1 st B = 2 nd A 𝑵 1 st B 𝑵 2 nd A
51 36 46 50 3eqtr4g 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A = 2 nd A 𝑵 2 nd A 𝑵 1 st B
52 mulasspi 2 nd A 𝑵 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 2 nd B
53 52 eqcomi 2 nd A 𝑵 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 2 nd B
54 53 a1i 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A 2 nd A 𝑵 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 2 nd B
55 51 54 opeq12d 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A 2 nd A 𝑵 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B
56 55 eqeq2d 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 1 st A 𝑵 2 nd A 𝑵 2 nd B + 𝑵 y 𝑵 2 nd A 2 nd A 𝑵 2 nd A 𝑵 2 nd B A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B
57 35 56 syl5ibcom A 𝑸 B 𝑸 y 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B
58 fveq2 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B / 𝑸 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = / 𝑸 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B
59 adderpq / 𝑸 A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = / 𝑸 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B
60 nqerid A 𝑸 / 𝑸 A = A
61 60 ad2antrr A 𝑸 B 𝑸 y 𝑵 / 𝑸 A = A
62 61 oveq1d A 𝑸 B 𝑸 y 𝑵 / 𝑸 A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B
63 59 62 eqtr3id A 𝑸 B 𝑸 y 𝑵 / 𝑸 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B
64 mulclpi 2 nd A 𝑵 2 nd A 𝑵 2 nd A 𝑵 2 nd A 𝑵
65 17 17 64 syl2anc A 𝑸 B 𝑸 2 nd A 𝑵 2 nd A 𝑵
66 65 adantr A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵
67 15 adantr A 𝑸 B 𝑸 y 𝑵 1 st B 𝑵
68 11 adantr A 𝑸 B 𝑸 y 𝑵 2 nd B 𝑵
69 mulcanenq 2 nd A 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd B 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B ~ 𝑸 1 st B 2 nd B
70 66 67 68 69 syl3anc A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B ~ 𝑸 1 st B 2 nd B
71 8 ad2antlr A 𝑸 B 𝑸 y 𝑵 B 𝑵 × 𝑵
72 1st2nd Rel 𝑵 × 𝑵 B 𝑵 × 𝑵 B = 1 st B 2 nd B
73 22 71 72 sylancr A 𝑸 B 𝑸 y 𝑵 B = 1 st B 2 nd B
74 70 73 breqtrrd A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B ~ 𝑸 B
75 mulclpi 2 nd A 𝑵 2 nd A 𝑵 1 st B 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 𝑵
76 66 67 75 syl2anc A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 𝑵
77 mulclpi 2 nd A 𝑵 2 nd A 𝑵 2 nd B 𝑵 2 nd A 𝑵 2 nd A 𝑵 2 nd B 𝑵
78 66 68 77 syl2anc A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵 2 nd B 𝑵
79 76 78 opelxpd A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B 𝑵 × 𝑵
80 nqereq 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B 𝑵 × 𝑵 B 𝑵 × 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B ~ 𝑸 B / 𝑸 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B = / 𝑸 B
81 79 71 80 syl2anc A 𝑸 B 𝑸 y 𝑵 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B ~ 𝑸 B / 𝑸 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B = / 𝑸 B
82 74 81 mpbid A 𝑸 B 𝑸 y 𝑵 / 𝑸 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B = / 𝑸 B
83 nqerid B 𝑸 / 𝑸 B = B
84 83 ad2antlr A 𝑸 B 𝑸 y 𝑵 / 𝑸 B = B
85 82 84 eqtrd A 𝑸 B 𝑸 y 𝑵 / 𝑸 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B = B
86 63 85 eqeq12d A 𝑸 B 𝑸 y 𝑵 / 𝑸 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = / 𝑸 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = B
87 58 86 syl5ib A 𝑸 B 𝑸 y 𝑵 A + 𝑝𝑸 y 2 nd A 𝑵 2 nd B = 2 nd A 𝑵 2 nd A 𝑵 1 st B 2 nd A 𝑵 2 nd A 𝑵 2 nd B A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = B
88 57 87 syld A 𝑸 B 𝑸 y 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = B
89 fvex / 𝑸 y 2 nd A 𝑵 2 nd B V
90 oveq2 x = / 𝑸 y 2 nd A 𝑵 2 nd B A + 𝑸 x = A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B
91 90 eqeq1d x = / 𝑸 y 2 nd A 𝑵 2 nd B A + 𝑸 x = B A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = B
92 89 91 spcev A + 𝑸 / 𝑸 y 2 nd A 𝑵 2 nd B = B x A + 𝑸 x = B
93 88 92 syl6 A 𝑸 B 𝑸 y 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A x A + 𝑸 x = B
94 93 rexlimdva A 𝑸 B 𝑸 y 𝑵 1 st A 𝑵 2 nd B + 𝑵 y = 1 st B 𝑵 2 nd A x A + 𝑸 x = B
95 21 94 sylbid A 𝑸 B 𝑸 1 st A 𝑵 2 nd B < 𝑵 1 st B 𝑵 2 nd A x A + 𝑸 x = B
96 3 95 sylbid A 𝑸 B 𝑸 A < 𝑸 B x A + 𝑸 x = B
97 2 96 mpcom A < 𝑸 B x A + 𝑸 x = B
98 eleq1 A + 𝑸 x = B A + 𝑸 x 𝑸 B 𝑸
99 98 biimparc B 𝑸 A + 𝑸 x = B A + 𝑸 x 𝑸
100 addnqf + 𝑸 : 𝑸 × 𝑸 𝑸
101 100 fdmi dom + 𝑸 = 𝑸 × 𝑸
102 0nnq ¬ 𝑸
103 101 102 ndmovrcl A + 𝑸 x 𝑸 A 𝑸 x 𝑸
104 ltaddnq A 𝑸 x 𝑸 A < 𝑸 A + 𝑸 x
105 99 103 104 3syl B 𝑸 A + 𝑸 x = B A < 𝑸 A + 𝑸 x
106 simpr B 𝑸 A + 𝑸 x = B A + 𝑸 x = B
107 105 106 breqtrd B 𝑸 A + 𝑸 x = B A < 𝑸 B
108 107 ex B 𝑸 A + 𝑸 x = B A < 𝑸 B
109 108 exlimdv B 𝑸 x A + 𝑸 x = B A < 𝑸 B
110 97 109 impbid2 B 𝑸 A < 𝑸 B x A + 𝑸 x = B