# Metamath Proof Explorer

## Theorem qbtwnxr

Description: The rational numbers are dense in RR* : any two extended real numbers have a rational between them. (Contributed by NM, 6-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion qbtwnxr ${⊢}\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 elxr ${⊢}{A}\in {ℝ}^{*}↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$
2 elxr ${⊢}{B}\in {ℝ}^{*}↔\left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)$
3 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)$
4 3 3expia ${⊢}\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)$
5 simpl ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to {A}\in ℝ$
6 peano2re ${⊢}{A}\in ℝ\to {A}+1\in ℝ$
7 6 adantr ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to {A}+1\in ℝ$
8 ltp1 ${⊢}{A}\in ℝ\to {A}<{A}+1$
9 8 adantr ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to {A}<{A}+1$
10 qbtwnre ${⊢}\left({A}\in ℝ\wedge {A}+1\in ℝ\wedge {A}<{A}+1\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{A}+1\right)$
11 5 7 9 10 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{A}+1\right)$
12 qre ${⊢}{x}\in ℚ\to {x}\in ℝ$
13 12 ltpnfd ${⊢}{x}\in ℚ\to {x}<\mathrm{+\infty }$
14 13 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\wedge {x}\in ℚ\right)\to {x}<\mathrm{+\infty }$
15 simplr ${⊢}\left(\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\wedge {x}\in ℚ\right)\to {B}=\mathrm{+\infty }$
16 14 15 breqtrrd ${⊢}\left(\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\wedge {x}\in ℚ\right)\to {x}<{B}$
17 16 a1d ${⊢}\left(\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\wedge {x}\in ℚ\right)\to \left({x}<{A}+1\to {x}<{B}\right)$
18 17 anim2d ${⊢}\left(\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\wedge {x}\in ℚ\right)\to \left(\left({A}<{x}\wedge {x}<{A}+1\right)\to \left({A}<{x}\wedge {x}<{B}\right)\right)$
19 18 reximdva ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to \left(\exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{A}+1\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
20 11 19 mpd ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
21 20 a1d ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{+\infty }\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
22 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
23 breq2 ${⊢}{B}=\mathrm{-\infty }\to \left({A}<{B}↔{A}<\mathrm{-\infty }\right)$
24 23 adantl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}↔{A}<\mathrm{-\infty }\right)$
25 nltmnf ${⊢}{A}\in {ℝ}^{*}\to ¬{A}<\mathrm{-\infty }$
26 25 adantr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to ¬{A}<\mathrm{-\infty }$
27 26 pm2.21d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<\mathrm{-\infty }\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
28 24 27 sylbid ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
29 22 28 sylan ${⊢}\left({A}\in ℝ\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
30 4 21 29 3jaodan ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
31 2 30 sylan2b ${⊢}\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)$
32 breq1 ${⊢}{A}=\mathrm{+\infty }\to \left({A}<{B}↔\mathrm{+\infty }<{B}\right)$
33 32 adantr ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}↔\mathrm{+\infty }<{B}\right)$
34 pnfnlt ${⊢}{B}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{B}$
35 34 adantl ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to ¬\mathrm{+\infty }<{B}$
36 35 pm2.21d ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left(\mathrm{+\infty }<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
37 33 36 sylbid ${⊢}\left({A}=\mathrm{+\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
38 peano2rem ${⊢}{B}\in ℝ\to {B}-1\in ℝ$
39 38 adantl ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to {B}-1\in ℝ$
40 simpr ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to {B}\in ℝ$
41 ltm1 ${⊢}{B}\in ℝ\to {B}-1<{B}$
42 41 adantl ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to {B}-1<{B}$
43 qbtwnre ${⊢}\left({B}-1\in ℝ\wedge {B}\in ℝ\wedge {B}-1<{B}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({B}-1<{x}\wedge {x}<{B}\right)$
44 39 40 42 43 syl3anc ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({B}-1<{x}\wedge {x}<{B}\right)$
45 simpll ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\wedge {x}\in ℚ\right)\to {A}=\mathrm{-\infty }$
46 12 adantl ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\wedge {x}\in ℚ\right)\to {x}\in ℝ$
47 46 mnfltd ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\wedge {x}\in ℚ\right)\to \mathrm{-\infty }<{x}$
48 45 47 eqbrtrd ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\wedge {x}\in ℚ\right)\to {A}<{x}$
49 48 a1d ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\wedge {x}\in ℚ\right)\to \left({B}-1<{x}\to {A}<{x}\right)$
50 49 anim1d ${⊢}\left(\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\wedge {x}\in ℚ\right)\to \left(\left({B}-1<{x}\wedge {x}<{B}\right)\to \left({A}<{x}\wedge {x}<{B}\right)\right)$
51 50 reximdva ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to \left(\exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({B}-1<{x}\wedge {x}<{B}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
52 44 51 mpd ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
53 52 a1d ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in ℝ\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
54 1re ${⊢}1\in ℝ$
55 mnflt ${⊢}1\in ℝ\to \mathrm{-\infty }<1$
56 54 55 ax-mp ${⊢}\mathrm{-\infty }<1$
57 breq1 ${⊢}{A}=\mathrm{-\infty }\to \left({A}<1↔\mathrm{-\infty }<1\right)$
58 56 57 mpbiri ${⊢}{A}=\mathrm{-\infty }\to {A}<1$
59 ltpnf ${⊢}1\in ℝ\to 1<\mathrm{+\infty }$
60 54 59 ax-mp ${⊢}1<\mathrm{+\infty }$
61 breq2 ${⊢}{B}=\mathrm{+\infty }\to \left(1<{B}↔1<\mathrm{+\infty }\right)$
62 60 61 mpbiri ${⊢}{B}=\mathrm{+\infty }\to 1<{B}$
63 1z ${⊢}1\in ℤ$
64 zq ${⊢}1\in ℤ\to 1\in ℚ$
65 63 64 ax-mp ${⊢}1\in ℚ$
66 breq2 ${⊢}{x}=1\to \left({A}<{x}↔{A}<1\right)$
67 breq1 ${⊢}{x}=1\to \left({x}<{B}↔1<{B}\right)$
68 66 67 anbi12d ${⊢}{x}=1\to \left(\left({A}<{x}\wedge {x}<{B}\right)↔\left({A}<1\wedge 1<{B}\right)\right)$
69 68 rspcev ${⊢}\left(1\in ℚ\wedge \left({A}<1\wedge 1<{B}\right)\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
70 65 69 mpan ${⊢}\left({A}<1\wedge 1<{B}\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
71 58 62 70 syl2an ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}=\mathrm{+\infty }\right)\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)$
72 71 a1d ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}=\mathrm{+\infty }\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
73 3mix3 ${⊢}{A}=\mathrm{-\infty }\to \left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$
74 73 1 sylibr ${⊢}{A}=\mathrm{-\infty }\to {A}\in {ℝ}^{*}$
75 74 28 sylan ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}=\mathrm{-\infty }\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
76 53 72 75 3jaodan ${⊢}\left({A}=\mathrm{-\infty }\wedge \left({B}\in ℝ\vee {B}=\mathrm{+\infty }\vee {B}=\mathrm{-\infty }\right)\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
77 2 76 sylan2b ${⊢}\left({A}=\mathrm{-\infty }\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
78 31 37 77 3jaoian ${⊢}\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)\wedge {B}\in {ℝ}^{*}\right)\to \left({A}<{B}\to \exists {x}\in ℚ\phantom{\rule{.4em}{0ex}}\left({A}<{x}\wedge {x}<{B}\right)\right)$
79 1 78 sylanb ${⊢}\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)$
80 79 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)$