qbtwnxr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > qbtwnxr		GIF version

Theorem qbtwnxr 10413

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 9911	. . 3 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 9911	. . . . 5 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		qbtwnre 10412	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
4	3	3expia 1208	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
5		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 ∈ ℝ)
6		peano2re 8221	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
7	6	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 + 1) ∈ ℝ)
8		ltp1 8930	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
9	8	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < (𝐴 + 1))
10		qbtwnre 10412	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ ∧ 𝐴 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)))
11	5, 7, 9, 10	syl3anc 1250	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)))
12		qre 9759	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
13		ltpnf 9915	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
14	12, 13	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑥 < +∞)
15	14	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < +∞)
16		simplr 528	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝐵 = +∞)
17	15, 16	breqtrrd 4076	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < 𝐵)
18	17	a1d 22	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → (𝑥 < (𝐴 + 1) → 𝑥 < 𝐵))
19	18	anim2d 337	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → ((𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
20	19	reximdva 2609	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
21	11, 20	mpd 13	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
22	21	a1d 22	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
23		rexr 8131	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
24		breq2 4052	. . . . . . . . 9 ⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
25	24	adantl 277	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
26		nltmnf 9923	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
27	26	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
28	27	pm2.21d 620	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < -∞ → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
29	25, 28	sylbid 150	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
30	23, 29	sylan 283	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
31	4, 22, 30	3jaodan 1319	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
32	2, 31	sylan2b 287	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
33		breq1 4051	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
34	33	adantr 276	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
35		pnfnlt 9922	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
36	35	adantl 277	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
37	36	pm2.21d 620	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
38	34, 37	sylbid 150	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
39		peano2rem 8352	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
40	39	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) ∈ ℝ)
41		simpr 110	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
42		ltm1 8932	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) < 𝐵)
43	42	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) < 𝐵)
44		qbtwnre 10412	. . . . . . . . 9 ⊢ (((𝐵 − 1) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐵 − 1) < 𝐵) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵))
45	40, 41, 43, 44	syl3anc 1250	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵))
46		simpll 527	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 = -∞)
47	12	adantl 277	. . . . . . . . . . . . 13 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝑥 ∈ ℝ)
48		mnflt 9918	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → -∞ < 𝑥)
49	47, 48	syl 14	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → -∞ < 𝑥)
50	46, 49	eqbrtrd 4070	. . . . . . . . . . 11 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 < 𝑥)
51	50	a1d 22	. . . . . . . . . 10 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → ((𝐵 − 1) < 𝑥 → 𝐴 < 𝑥))
52	51	anim1d 336	. . . . . . . . 9 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → (((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
53	52	reximdva 2609	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
54	45, 53	mpd 13	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
55	54	a1d 22	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
56		1re 8084	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
57		mnflt 9918	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → -∞ < 1)
58	56, 57	ax-mp 5	. . . . . . . . 9 ⊢ -∞ < 1
59		breq1 4051	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 < 1 ↔ -∞ < 1))
60	58, 59	mpbiri 168	. . . . . . . 8 ⊢ (𝐴 = -∞ → 𝐴 < 1)
61		ltpnf 9915	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → 1 < +∞)
62	56, 61	ax-mp 5	. . . . . . . . 9 ⊢ 1 < +∞
63		breq2 4052	. . . . . . . . 9 ⊢ (𝐵 = +∞ → (1 < 𝐵 ↔ 1 < +∞))
64	62, 63	mpbiri 168	. . . . . . . 8 ⊢ (𝐵 = +∞ → 1 < 𝐵)
65		1z 9411	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
66		zq 9760	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ 1 ∈ ℚ
68		breq2 4052	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐴 < 𝑥 ↔ 𝐴 < 1))
69		breq1 4051	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 < 𝐵 ↔ 1 < 𝐵))
70	68, 69	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 1 ∧ 1 < 𝐵)))
71	70	rspcev 2879	. . . . . . . . 9 ⊢ ((1 ∈ ℚ ∧ (𝐴 < 1 ∧ 1 < 𝐵)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
72	67, 71	mpan 424	. . . . . . . 8 ⊢ ((𝐴 < 1 ∧ 1 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
73	60, 64, 72	syl2an 289	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
74	73	a1d 22	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
75		3mix3 1171	. . . . . . . 8 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
76	75, 1	sylibr 134	. . . . . . 7 ⊢ (𝐴 = -∞ → 𝐴 ∈ ℝ^*)
77	76, 29	sylan 283	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
78	55, 74, 77	3jaodan 1319	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
79	2, 78	sylan2b 287	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
80	32, 38, 79	3jaoian 1318	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
81	1, 80	sylanb 284	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
82	81	3impia 1203	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ w3o 980 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 ∃wrex 2486 class class class wbr 4048 (class class class)co 5954 ℝcr 7937 1c1 7939 + caddc 7941 +∞cpnf 8117 -∞cmnf 8118 ℝ^*cxr 8119 < clt 8120 − cmin 8256 ℤcz 9385 ℚcq 9753

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4167 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053 ax-pre-ltadd 8054 ax-pre-mulgt0 8055 ax-pre-mulext 8056 ax-arch 8057

This theorem depends on definitions: df-bi 117 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3001 df-csb 3096 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-int 3889 df-iun 3932 df-br 4049 df-opab 4111 df-mpt 4112 df-id 4345 df-po 4348 df-iso 4349 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-ima 4693 df-iota 5238 df-fun 5279 df-fn 5280 df-f 5281 df-fv 5285 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-1st 6236 df-2nd 6237 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126 df-sub 8258 df-neg 8259 df-reap 8661 df-ap 8668 df-div 8759 df-inn 9050 df-2 9108 df-n0 9309 df-z 9386 df-uz 9662 df-q 9754 df-rp 9789

This theorem is referenced by: ioo0 10415 ioom 10416 ico0 10417 ioc0 10418 blssps 14949 blss 14950 tgqioo 15077

W3C validator