# Metamath Proof Explorer

## Theorem qbtwnre

Description: The rational numbers are dense in RR : any two real numbers have a rational between them. Exercise 6 of Apostol p. 28. (Contributed by NM, 18-Nov-2004) (Proof shortened by Mario Carneiro, 13-Jun-2014)

Ref Expression
Assertion qbtwnre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$

### Proof

Step Hyp Ref Expression
1 posdif ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔0<{B}-{A}\right)$
2 resubcl ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to {B}-{A}\in ℝ$
3 nnrecl ${⊢}\left({B}-{A}\in ℝ\wedge 0<{B}-{A}\right)\to \exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{y}}<{B}-{A}$
4 2 3 sylan ${⊢}\left(\left({B}\in ℝ\wedge {A}\in ℝ\right)\wedge 0<{B}-{A}\right)\to \exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{y}}<{B}-{A}$
5 4 ex ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to \left(0<{B}-{A}\to \exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{y}}<{B}-{A}\right)$
6 5 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0<{B}-{A}\to \exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{y}}<{B}-{A}\right)$
7 1 6 sylbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}\to \exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{y}}<{B}-{A}\right)$
8 nnre ${⊢}{y}\in ℕ\to {y}\in ℝ$
9 8 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to {y}\in ℝ$
10 simplr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to {B}\in ℝ$
11 9 10 remulcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to {y}{B}\in ℝ$
12 peano2rem ${⊢}{y}{B}\in ℝ\to {y}{B}-1\in ℝ$
13 11 12 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to {y}{B}-1\in ℝ$
14 zbtwnre ${⊢}{y}{B}-1\in ℝ\to \exists !{z}\in ℤ\phantom{\rule{.4em}{0ex}}\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)$
15 reurex ${⊢}\exists !{z}\in ℤ\phantom{\rule{.4em}{0ex}}\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\to \exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)$
16 13 14 15 3syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to \exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)$
17 znq ${⊢}\left({z}\in ℤ\wedge {y}\in ℕ\right)\to \frac{{z}}{{y}}\in ℚ$
18 17 ancoms ${⊢}\left({y}\in ℕ\wedge {z}\in ℤ\right)\to \frac{{z}}{{y}}\in ℚ$
19 18 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \frac{{z}}{{y}}\in ℚ$
20 an32 ${⊢}\left(\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\wedge \frac{1}{{y}}<{B}-{A}\right)↔\left(\left({y}{B}-1\le {z}\wedge \frac{1}{{y}}<{B}-{A}\right)\wedge {z}<{y}{B}-1+1\right)$
21 8 ad2antrl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}\in ℝ$
22 simpll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {A}\in ℝ$
23 21 22 remulcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}{A}\in ℝ$
24 13 adantrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}{B}-1\in ℝ$
25 zre ${⊢}{z}\in ℤ\to {z}\in ℝ$
26 25 ad2antll ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {z}\in ℝ$
27 ltletr ${⊢}\left({y}{A}\in ℝ\wedge {y}{B}-1\in ℝ\wedge {z}\in ℝ\right)\to \left(\left({y}{A}<{y}{B}-1\wedge {y}{B}-1\le {z}\right)\to {y}{A}<{z}\right)$
28 23 24 26 27 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left({y}{A}<{y}{B}-1\wedge {y}{B}-1\le {z}\right)\to {y}{A}<{z}\right)$
29 21 recnd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}\in ℂ$
30 simplr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {B}\in ℝ$
31 30 recnd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {B}\in ℂ$
32 22 recnd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {A}\in ℂ$
33 29 31 32 subdid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}\left({B}-{A}\right)={y}{B}-{y}{A}$
34 33 breq2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(1<{y}\left({B}-{A}\right)↔1<{y}{B}-{y}{A}\right)$
35 1red ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to 1\in ℝ$
36 30 22 resubcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {B}-{A}\in ℝ$
37 nngt0 ${⊢}{y}\in ℕ\to 0<{y}$
38 37 ad2antrl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to 0<{y}$
39 ltdivmul ${⊢}\left(1\in ℝ\wedge {B}-{A}\in ℝ\wedge \left({y}\in ℝ\wedge 0<{y}\right)\right)\to \left(\frac{1}{{y}}<{B}-{A}↔1<{y}\left({B}-{A}\right)\right)$
40 35 36 21 38 39 syl112anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\frac{1}{{y}}<{B}-{A}↔1<{y}\left({B}-{A}\right)\right)$
41 11 adantrr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}{B}\in ℝ$
42 ltsub13 ${⊢}\left({y}{A}\in ℝ\wedge {y}{B}\in ℝ\wedge 1\in ℝ\right)\to \left({y}{A}<{y}{B}-1↔1<{y}{B}-{y}{A}\right)$
43 23 41 35 42 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left({y}{A}<{y}{B}-1↔1<{y}{B}-{y}{A}\right)$
44 34 40 43 3bitr4rd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left({y}{A}<{y}{B}-1↔\frac{1}{{y}}<{B}-{A}\right)$
45 44 anbi1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left({y}{A}<{y}{B}-1\wedge {y}{B}-1\le {z}\right)↔\left(\frac{1}{{y}}<{B}-{A}\wedge {y}{B}-1\le {z}\right)\right)$
46 45 biancomd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left({y}{A}<{y}{B}-1\wedge {y}{B}-1\le {z}\right)↔\left({y}{B}-1\le {z}\wedge \frac{1}{{y}}<{B}-{A}\right)\right)$
47 ltmuldiv2 ${⊢}\left({A}\in ℝ\wedge {z}\in ℝ\wedge \left({y}\in ℝ\wedge 0<{y}\right)\right)\to \left({y}{A}<{z}↔{A}<\frac{{z}}{{y}}\right)$
48 22 26 21 38 47 syl112anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left({y}{A}<{z}↔{A}<\frac{{z}}{{y}}\right)$
49 28 46 48 3imtr3d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left({y}{B}-1\le {z}\wedge \frac{1}{{y}}<{B}-{A}\right)\to {A}<\frac{{z}}{{y}}\right)$
50 41 recnd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}{B}\in ℂ$
51 ax-1cn ${⊢}1\in ℂ$
52 npcan ${⊢}\left({y}{B}\in ℂ\wedge 1\in ℂ\right)\to {y}{B}-1+1={y}{B}$
53 50 51 52 sylancl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to {y}{B}-1+1={y}{B}$
54 53 breq2d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left({z}<{y}{B}-1+1↔{z}<{y}{B}\right)$
55 ltdivmul ${⊢}\left({z}\in ℝ\wedge {B}\in ℝ\wedge \left({y}\in ℝ\wedge 0<{y}\right)\right)\to \left(\frac{{z}}{{y}}<{B}↔{z}<{y}{B}\right)$
56 26 30 21 38 55 syl112anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\frac{{z}}{{y}}<{B}↔{z}<{y}{B}\right)$
57 54 56 bitr4d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left({z}<{y}{B}-1+1↔\frac{{z}}{{y}}<{B}\right)$
58 57 biimpd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left({z}<{y}{B}-1+1\to \frac{{z}}{{y}}<{B}\right)$
59 49 58 anim12d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left(\left({y}{B}-1\le {z}\wedge \frac{1}{{y}}<{B}-{A}\right)\wedge {z}<{y}{B}-1+1\right)\to \left({A}<\frac{{z}}{{y}}\wedge \frac{{z}}{{y}}<{B}\right)\right)$
60 20 59 syl5bi ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left(\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\wedge \frac{1}{{y}}<{B}-{A}\right)\to \left({A}<\frac{{z}}{{y}}\wedge \frac{{z}}{{y}}<{B}\right)\right)$
61 breq2 ${⊢}{x}=\frac{{z}}{{y}}\to \left({A}<{x}↔{A}<\frac{{z}}{{y}}\right)$
62 breq1 ${⊢}{x}=\frac{{z}}{{y}}\to \left({x}<{B}↔\frac{{z}}{{y}}<{B}\right)$
63 61 62 anbi12d ${⊢}{x}=\frac{{z}}{{y}}\to \left(\left({A}<{x}\wedge {x}<{B}\right)↔\left({A}<\frac{{z}}{{y}}\wedge \frac{{z}}{{y}}<{B}\right)\right)$
64 63 rspcev ${⊢}\left(\frac{{z}}{{y}}\in ℚ\wedge \left({A}<\frac{{z}}{{y}}\wedge \frac{{z}}{{y}}<{B}\right)\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
65 19 60 64 syl6an ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left(\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\wedge \frac{1}{{y}}<{B}-{A}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
66 65 expd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({y}\in ℕ\wedge {z}\in ℤ\right)\right)\to \left(\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\to \left(\frac{1}{{y}}<{B}-{A}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)\right)$
67 66 expr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to \left({z}\in ℤ\to \left(\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\to \left(\frac{1}{{y}}<{B}-{A}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)\right)\right)$
68 67 rexlimdv ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to \left(\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\left({y}{B}-1\le {z}\wedge {z}<{y}{B}-1+1\right)\to \left(\frac{1}{{y}}<{B}-{A}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)\right)$
69 16 68 mpd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {y}\in ℕ\right)\to \left(\frac{1}{{y}}<{B}-{A}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
70 69 rexlimdva ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{y}}<{B}-{A}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
71 7 70 syld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
72 71 3impia ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$