Metamath Proof Explorer


Theorem ltbtwnnq

Description: There exists a number between any two positive fractions. Proposition 9-2.6(i) of Gleason p. 120. (Contributed by NM, 17-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion ltbtwnnq A < 𝑸 B x A < 𝑸 x x < 𝑸 B

Proof

Step Hyp Ref Expression
1 ltrelnq < 𝑸 𝑸 × 𝑸
2 1 brel A < 𝑸 B A 𝑸 B 𝑸
3 2 simprd A < 𝑸 B B 𝑸
4 ltexnq B 𝑸 A < 𝑸 B y A + 𝑸 y = B
5 eleq1 A + 𝑸 y = B A + 𝑸 y 𝑸 B 𝑸
6 5 biimparc B 𝑸 A + 𝑸 y = B A + 𝑸 y 𝑸
7 addnqf + 𝑸 : 𝑸 × 𝑸 𝑸
8 7 fdmi dom + 𝑸 = 𝑸 × 𝑸
9 0nnq ¬ 𝑸
10 8 9 ndmovrcl A + 𝑸 y 𝑸 A 𝑸 y 𝑸
11 6 10 syl B 𝑸 A + 𝑸 y = B A 𝑸 y 𝑸
12 11 simprd B 𝑸 A + 𝑸 y = B y 𝑸
13 nsmallnq y 𝑸 z z < 𝑸 y
14 11 simpld B 𝑸 A + 𝑸 y = B A 𝑸
15 1 brel z < 𝑸 y z 𝑸 y 𝑸
16 15 simpld z < 𝑸 y z 𝑸
17 ltaddnq A 𝑸 z 𝑸 A < 𝑸 A + 𝑸 z
18 14 16 17 syl2an B 𝑸 A + 𝑸 y = B z < 𝑸 y A < 𝑸 A + 𝑸 z
19 ltanq A 𝑸 z < 𝑸 y A + 𝑸 z < 𝑸 A + 𝑸 y
20 19 biimpa A 𝑸 z < 𝑸 y A + 𝑸 z < 𝑸 A + 𝑸 y
21 14 20 sylan B 𝑸 A + 𝑸 y = B z < 𝑸 y A + 𝑸 z < 𝑸 A + 𝑸 y
22 simplr B 𝑸 A + 𝑸 y = B z < 𝑸 y A + 𝑸 y = B
23 21 22 breqtrd B 𝑸 A + 𝑸 y = B z < 𝑸 y A + 𝑸 z < 𝑸 B
24 ovex A + 𝑸 z V
25 breq2 x = A + 𝑸 z A < 𝑸 x A < 𝑸 A + 𝑸 z
26 breq1 x = A + 𝑸 z x < 𝑸 B A + 𝑸 z < 𝑸 B
27 25 26 anbi12d x = A + 𝑸 z A < 𝑸 x x < 𝑸 B A < 𝑸 A + 𝑸 z A + 𝑸 z < 𝑸 B
28 24 27 spcev A < 𝑸 A + 𝑸 z A + 𝑸 z < 𝑸 B x A < 𝑸 x x < 𝑸 B
29 18 23 28 syl2anc B 𝑸 A + 𝑸 y = B z < 𝑸 y x A < 𝑸 x x < 𝑸 B
30 29 ex B 𝑸 A + 𝑸 y = B z < 𝑸 y x A < 𝑸 x x < 𝑸 B
31 30 exlimdv B 𝑸 A + 𝑸 y = B z z < 𝑸 y x A < 𝑸 x x < 𝑸 B
32 13 31 syl5 B 𝑸 A + 𝑸 y = B y 𝑸 x A < 𝑸 x x < 𝑸 B
33 12 32 mpd B 𝑸 A + 𝑸 y = B x A < 𝑸 x x < 𝑸 B
34 33 ex B 𝑸 A + 𝑸 y = B x A < 𝑸 x x < 𝑸 B
35 34 exlimdv B 𝑸 y A + 𝑸 y = B x A < 𝑸 x x < 𝑸 B
36 4 35 sylbid B 𝑸 A < 𝑸 B x A < 𝑸 x x < 𝑸 B
37 3 36 mpcom A < 𝑸 B x A < 𝑸 x x < 𝑸 B
38 ltsonq < 𝑸 Or 𝑸
39 38 1 sotri A < 𝑸 x x < 𝑸 B A < 𝑸 B
40 39 exlimiv x A < 𝑸 x x < 𝑸 B A < 𝑸 B
41 37 40 impbii A < 𝑸 B x A < 𝑸 x x < 𝑸 B