qbtwnxr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > qbtwnxr		Structured version Visualization version GIF version

Theorem qbtwnxr 13127

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

**Assertion**
Ref	Expression
qbtwnxr	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

**Proof of Theorem qbtwnxr**
Step	Hyp	Ref	Expression
1		elxr 13042	. . 3 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13042	. . . . 5 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		qbtwnre 13126	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
4	3	3expia 1122	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
5		simpl 482	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 ∈ ℝ)
6		peano2re 11318	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
7	6	adantr 480	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 + 1) ∈ ℝ)
8		ltp1 11993	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
9	8	adantr 480	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < (𝐴 + 1))
10		qbtwnre 13126	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ ∧ 𝐴 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)))
11	5, 7, 9, 10	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)))
12		qre 12878	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
13	12	ltpnfd 13047	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑥 < +∞)
14	13	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < +∞)
15		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝐵 = +∞)
16	14, 15	breqtrrd 5128	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < 𝐵)
17	16	a1d 25	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → (𝑥 < (𝐴 + 1) → 𝑥 < 𝐵))
18	17	anim2d 613	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → ((𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
19	18	reximdva 3151	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
20	11, 19	mpd 15	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
21	20	a1d 25	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
22		rexr 11190	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
23		breq2 5104	. . . . . . . . 9 ⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
24	23	adantl 481	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
25		nltmnf 13055	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
26	25	adantr 480	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
27	26	pm2.21d 121	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < -∞ → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
28	24, 27	sylbid 240	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
29	22, 28	sylan 581	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
30	4, 21, 29	3jaodan 1434	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
31	2, 30	sylan2b 595	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
32		breq1 5103	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
33	32	adantr 480	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
34		pnfnlt 13054	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
35	34	adantl 481	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
36	35	pm2.21d 121	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
37	33, 36	sylbid 240	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
38		peano2rem 11460	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
39	38	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) ∈ ℝ)
40		simpr 484	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
41		ltm1 11995	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) < 𝐵)
42	41	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) < 𝐵)
43		qbtwnre 13126	. . . . . . . . 9 ⊢ (((𝐵 − 1) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐵 − 1) < 𝐵) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵))
44	39, 40, 42, 43	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵))
45		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 = -∞)
46	12	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝑥 ∈ ℝ)
47	46	mnfltd 13050	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → -∞ < 𝑥)
48	45, 47	eqbrtrd 5122	. . . . . . . . . . 11 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 < 𝑥)
49	48	a1d 25	. . . . . . . . . 10 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → ((𝐵 − 1) < 𝑥 → 𝐴 < 𝑥))
50	49	anim1d 612	. . . . . . . . 9 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → (((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
51	50	reximdva 3151	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
52	44, 51	mpd 15	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
53	52	a1d 25	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
54		1re 11144	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
55		mnflt 13049	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → -∞ < 1)
56	54, 55	ax-mp 5	. . . . . . . . 9 ⊢ -∞ < 1
57		breq1 5103	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 < 1 ↔ -∞ < 1))
58	56, 57	mpbiri 258	. . . . . . . 8 ⊢ (𝐴 = -∞ → 𝐴 < 1)
59		ltpnf 13046	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → 1 < +∞)
60	54, 59	ax-mp 5	. . . . . . . . 9 ⊢ 1 < +∞
61		breq2 5104	. . . . . . . . 9 ⊢ (𝐵 = +∞ → (1 < 𝐵 ↔ 1 < +∞))
62	60, 61	mpbiri 258	. . . . . . . 8 ⊢ (𝐵 = +∞ → 1 < 𝐵)
63		1z 12533	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
64		zq 12879	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
65	63, 64	ax-mp 5	. . . . . . . . 9 ⊢ 1 ∈ ℚ
66		breq2 5104	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐴 < 𝑥 ↔ 𝐴 < 1))
67		breq1 5103	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 < 𝐵 ↔ 1 < 𝐵))
68	66, 67	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 1 ∧ 1 < 𝐵)))
69	68	rspcev 3578	. . . . . . . . 9 ⊢ ((1 ∈ ℚ ∧ (𝐴 < 1 ∧ 1 < 𝐵)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
70	65, 69	mpan 691	. . . . . . . 8 ⊢ ((𝐴 < 1 ∧ 1 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
71	58, 62, 70	syl2an 597	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
72	71	a1d 25	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
73		3mix3 1334	. . . . . . . 8 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
74	73, 1	sylibr 234	. . . . . . 7 ⊢ (𝐴 = -∞ → 𝐴 ∈ ℝ^*)
75	74, 28	sylan 581	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
76	53, 72, 75	3jaodan 1434	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
77	2, 76	sylan2b 595	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
78	31, 37, 77	3jaoian 1433	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
79	1, 78	sylanb 582	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
80	79	3impia 1118	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ w3o 1086 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 class class class wbr 5100 (class class class)co 7368 ℝcr 11037 1c1 11039 + caddc 11041 +∞cpnf 11175 -∞cmnf 11176 ℝ^*cxr 11177 < clt 11178 − cmin 11376 ℤcz 12500 ℚcq 12873

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-sup 9357 df-inf 9358 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-n0 12414 df-z 12501 df-uz 12764 df-q 12874

This theorem is referenced by: qextltlem 13129 xralrple 13132 ixxub 13294 ixxlb 13295 ioo0 13298 ico0 13319 ioc0 13320 blssps 24380 blss 24381 blcld 24461 qdensere 24725 tgqioo 24756 dvlip2 25968 lhop2 25988 itgsubst 26024 itg2gt0cn 37923 qinioo 45892 qelioo 45903 qndenserrnbllem 46649

W3C validator