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↔∃xA+𝑸x=B

Proof

Step Hyp Ref Expression
1 ltrelnq ⊢<𝑸⊆𝑸×𝑸
2 1 brel ⊢A<𝑸B→A∈𝑸∧B∈𝑸
3 ordpinq ⊢A∈𝑸∧B∈𝑸→A<𝑸B↔1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A
4 elpqn ⊢A∈𝑸→A∈𝑵×𝑵
5 4 adantr ⊢A∈𝑸∧B∈𝑸→A∈𝑵×𝑵
6 xp1st ⊢A∈𝑵×𝑵→1st⁡A∈𝑵
7 5 6 syl ⊢A∈𝑸∧B∈𝑸→1st⁡A∈𝑵
8 elpqn ⊢B∈𝑸→B∈𝑵×𝑵
9 8 adantl ⊢A∈𝑸∧B∈𝑸→B∈𝑵×𝑵
10 xp2nd ⊢B∈𝑵×𝑵→2nd⁡B∈𝑵
11 9 10 syl ⊢A∈𝑸∧B∈𝑸→2nd⁡B∈𝑵
12 mulclpi ⊢1st⁡A∈𝑵∧2nd⁡B∈𝑵→1st⁡A⋅𝑵2nd⁡B∈𝑵
13 7 11 12 syl2anc ⊢A∈𝑸∧B∈𝑸→1st⁡A⋅𝑵2nd⁡B∈𝑵
14 xp1st ⊢B∈𝑵×𝑵→1st⁡B∈𝑵
15 9 14 syl ⊢A∈𝑸∧B∈𝑸→1st⁡B∈𝑵
16 xp2nd ⊢A∈𝑵×𝑵→2nd⁡A∈𝑵
17 5 16 syl ⊢A∈𝑸∧B∈𝑸→2nd⁡A∈𝑵
18 mulclpi ⊢1st⁡B∈𝑵∧2nd⁡A∈𝑵→1st⁡B⋅𝑵2nd⁡A∈𝑵
19 15 17 18 syl2anc ⊢A∈𝑸∧B∈𝑸→1st⁡B⋅𝑵2nd⁡A∈𝑵
20 ltexpi ⊢1st⁡A⋅𝑵2nd⁡B∈𝑵∧1st⁡B⋅𝑵2nd⁡A∈𝑵→1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A↔∃y∈𝑵1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A
21 13 19 20 syl2anc ⊢A∈𝑸∧B∈𝑸→1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A↔∃y∈𝑵1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A
22 relxp ⊢Rel⁡𝑵×𝑵
23 4 ad2antrr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→A∈𝑵×𝑵
24 1st2nd ⊢Rel⁡𝑵×𝑵∧A∈𝑵×𝑵→A=1st⁡A2nd⁡A
25 22 23 24 sylancr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→A=1st⁡A2nd⁡A
26 25 oveq1d ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=1st⁡A2nd⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B
27 7 adantr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→1st⁡A∈𝑵
28 17 adantr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A∈𝑵
29 simpr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→y∈𝑵
30 mulclpi ⊢2nd⁡A∈𝑵∧2nd⁡B∈𝑵→2nd⁡A⋅𝑵2nd⁡B∈𝑵
31 17 11 30 syl2anc ⊢A∈𝑸∧B∈𝑸→2nd⁡A⋅𝑵2nd⁡B∈𝑵
32 31 adantr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡B∈𝑵
33 addpipq ⊢1st⁡A∈𝑵∧2nd⁡A∈𝑵∧y∈𝑵∧2nd⁡A⋅𝑵2nd⁡B∈𝑵→1st⁡A2nd⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
34 27 28 29 32 33 syl22anc ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→1st⁡A2nd⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
35 26 34 eqtrd ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
36 oveq2 ⊢1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→2nd⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B+𝑵y=2nd⁡A⋅𝑵1st⁡B⋅𝑵2nd⁡A
37 distrpi ⊢2nd⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B+𝑵y=2nd⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B+𝑵2nd⁡A⋅𝑵y
38 fvex ⊢2nd⁡A∈V
39 fvex ⊢1st⁡A∈V
40 fvex ⊢2nd⁡B∈V
41 mulcompi ⊢x⋅𝑵y=y⋅𝑵x
42 mulasspi ⊢x⋅𝑵y⋅𝑵z=x⋅𝑵y⋅𝑵z
43 38 39 40 41 42 caov12 ⊢2nd⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
44 mulcompi ⊢2nd⁡A⋅𝑵y=y⋅𝑵2nd⁡A
45 43 44 oveq12i ⊢2nd⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B+𝑵2nd⁡A⋅𝑵y=1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A
46 37 45 eqtr2i ⊢1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A=2nd⁡A⋅𝑵1st⁡A⋅𝑵2nd⁡B+𝑵y
47 mulasspi ⊢2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B
48 mulcompi ⊢2nd⁡A⋅𝑵1st⁡B=1st⁡B⋅𝑵2nd⁡A
49 48 oveq2i ⊢2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B=2nd⁡A⋅𝑵1st⁡B⋅𝑵2nd⁡A
50 47 49 eqtri ⊢2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B=2nd⁡A⋅𝑵1st⁡B⋅𝑵2nd⁡A
51 36 46 50 3eqtr4g ⊢1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B
52 mulasspi ⊢2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
53 52 eqcomi ⊢2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
54 53 a1i ⊢1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
55 51 54 opeq12d ⊢1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
56 55 eqeq2d ⊢1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=1st⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B+𝑵y⋅𝑵2nd⁡A2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B↔A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
57 35 56 syl5ibcom ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
58 fveq2 ⊢A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B→/𝑸⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=/𝑸⁡2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B
59 adderpq ⊢/𝑸⁡A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=/𝑸⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B
60 nqerid ⊢A∈𝑸→/𝑸⁡A=A
61 60 ad2antrr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡A=A
62 61 oveq1d ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B
63 59 62 eqtr3id ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B
64 mulclpi ⊢2nd⁡A∈𝑵∧2nd⁡A∈𝑵→2nd⁡A⋅𝑵2nd⁡A∈𝑵
65 17 17 64 syl2anc ⊢A∈𝑸∧B∈𝑸→2nd⁡A⋅𝑵2nd⁡A∈𝑵
66 65 adantr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A∈𝑵
67 15 adantr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→1st⁡B∈𝑵
68 11 adantr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡B∈𝑵
69 mulcanenq ⊢2nd⁡A⋅𝑵2nd⁡A∈𝑵∧1st⁡B∈𝑵∧2nd⁡B∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B~𝑸1st⁡B2nd⁡B
70 66 67 68 69 syl3anc ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B~𝑸1st⁡B2nd⁡B
71 8 ad2antlr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→B∈𝑵×𝑵
72 1st2nd ⊢Rel⁡𝑵×𝑵∧B∈𝑵×𝑵→B=1st⁡B2nd⁡B
73 22 71 72 sylancr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→B=1st⁡B2nd⁡B
74 70 73 breqtrrd ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B~𝑸B
75 mulclpi ⊢2nd⁡A⋅𝑵2nd⁡A∈𝑵∧1st⁡B∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B∈𝑵
76 66 67 75 syl2anc ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B∈𝑵
77 mulclpi ⊢2nd⁡A⋅𝑵2nd⁡A∈𝑵∧2nd⁡B∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B∈𝑵
78 66 68 77 syl2anc ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B∈𝑵
79 76 78 opelxpd ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B∈𝑵×𝑵
80 nqereq ⊢2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B∈𝑵×𝑵∧B∈𝑵×𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B~𝑸B↔/𝑸⁡2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=/𝑸⁡B
81 79 71 80 syl2anc ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B~𝑸B↔/𝑸⁡2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=/𝑸⁡B
82 74 81 mpbid ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=/𝑸⁡B
83 nqerid ⊢B∈𝑸→/𝑸⁡B=B
84 83 ad2antlr ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡B=B
85 82 84 eqtrd ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B=B
86 63 85 eqeq12d ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→/𝑸⁡A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=/𝑸⁡2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B↔A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=B
87 58 86 imbitrid ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→A+𝑝𝑸y2nd⁡A⋅𝑵2nd⁡B=2nd⁡A⋅𝑵2nd⁡A⋅𝑵1st⁡B2nd⁡A⋅𝑵2nd⁡A⋅𝑵2nd⁡B→A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=B
88 57 87 syld ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=B
89 fvex ⊢/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B∈V
90 oveq2 ⊢x=/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B→A+𝑸x=A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B
91 90 eqeq1d ⊢x=/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B→A+𝑸x=B↔A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=B
92 89 91 spcev ⊢A+𝑸/𝑸⁡y2nd⁡A⋅𝑵2nd⁡B=B→∃xA+𝑸x=B
93 88 92 syl6 ⊢A∈𝑸∧B∈𝑸∧y∈𝑵→1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→∃xA+𝑸x=B
94 93 rexlimdva ⊢A∈𝑸∧B∈𝑸→∃y∈𝑵1st⁡A⋅𝑵2nd⁡B+𝑵y=1st⁡B⋅𝑵2nd⁡A→∃xA+𝑸x=B
95 21 94 sylbid ⊢A∈𝑸∧B∈𝑸→1st⁡A⋅𝑵2nd⁡B<𝑵1st⁡B⋅𝑵2nd⁡A→∃xA+𝑸x=B
96 3 95 sylbid ⊢A∈𝑸∧B∈𝑸→A<𝑸B→∃xA+𝑸x=B
97 2 96 mpcom ⊢A<𝑸B→∃xA+𝑸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∈𝑸→∃xA+𝑸x=B→A<𝑸B
110 97 109 impbid2 ⊢B∈𝑸→A<𝑸B↔∃xA+𝑸x=B