qbtwnxr - Intuitionistic Logic Explorer

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

Theorem qbtwnxr 10364

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 9868	. . 3 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 9868	. . . . 5 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		qbtwnre 10363	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
4	3	3expia 1207	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
5		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 ∈ ℝ)
6		peano2re 8179	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
7	6	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 + 1) ∈ ℝ)
8		ltp1 8888	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
9	8	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < (𝐴 + 1))
10		qbtwnre 10363	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ ∧ 𝐴 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)))
11	5, 7, 9, 10	syl3anc 1249	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)))
12		qre 9716	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
13		ltpnf 9872	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
14	12, 13	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑥 < +∞)
15	14	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < +∞)
16		simplr 528	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝐵 = +∞)
17	15, 16	breqtrrd 4062	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → 𝑥 < 𝐵)
18	17	a1d 22	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → (𝑥 < (𝐴 + 1) → 𝑥 < 𝐵))
19	18	anim2d 337	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∧ 𝑥 ∈ ℚ) → ((𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
20	19	reximdva 2599	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < (𝐴 + 1)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
21	11, 20	mpd 13	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
22	21	a1d 22	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
23		rexr 8089	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
24		breq2 4038	. . . . . . . . 9 ⊢ (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
25	24	adantl 277	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
26		nltmnf 9880	. . . . . . . . . 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 1317	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
32	2, 31	sylan2b 287	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
33		breq1 4037	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
34	33	adantr 276	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
35		pnfnlt 9879	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
36	35	adantl 277	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
37	36	pm2.21d 620	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
38	34, 37	sylbid 150	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
39		peano2rem 8310	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
40	39	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) ∈ ℝ)
41		simpr 110	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
42		ltm1 8890	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) < 𝐵)
43	42	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 − 1) < 𝐵)
44		qbtwnre 10363	. . . . . . . . 9 ⊢ (((𝐵 − 1) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐵 − 1) < 𝐵) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵))
45	40, 41, 43, 44	syl3anc 1249	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵))
46		simpll 527	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 = -∞)
47	12	adantl 277	. . . . . . . . . . . . 13 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝑥 ∈ ℝ)
48		mnflt 9875	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → -∞ < 𝑥)
49	47, 48	syl 14	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → -∞ < 𝑥)
50	46, 49	eqbrtrd 4056	. . . . . . . . . . 11 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → 𝐴 < 𝑥)
51	50	a1d 22	. . . . . . . . . 10 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → ((𝐵 − 1) < 𝑥 → 𝐴 < 𝑥))
52	51	anim1d 336	. . . . . . . . 9 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℚ) → (((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
53	52	reximdva 2599	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (∃𝑥 ∈ ℚ ((𝐵 − 1) < 𝑥 ∧ 𝑥 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
54	45, 53	mpd 13	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
55	54	a1d 22	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
56		1re 8042	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
57		mnflt 9875	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → -∞ < 1)
58	56, 57	ax-mp 5	. . . . . . . . 9 ⊢ -∞ < 1
59		breq1 4037	. . . . . . . . 9 ⊢ (𝐴 = -∞ → (𝐴 < 1 ↔ -∞ < 1))
60	58, 59	mpbiri 168	. . . . . . . 8 ⊢ (𝐴 = -∞ → 𝐴 < 1)
61		ltpnf 9872	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → 1 < +∞)
62	56, 61	ax-mp 5	. . . . . . . . 9 ⊢ 1 < +∞
63		breq2 4038	. . . . . . . . 9 ⊢ (𝐵 = +∞ → (1 < 𝐵 ↔ 1 < +∞))
64	62, 63	mpbiri 168	. . . . . . . 8 ⊢ (𝐵 = +∞ → 1 < 𝐵)
65		1z 9369	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
66		zq 9717	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ 1 ∈ ℚ
68		breq2 4038	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐴 < 𝑥 ↔ 𝐴 < 1))
69		breq1 4037	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 < 𝐵 ↔ 1 < 𝐵))
70	68, 69	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 1 ∧ 1 < 𝐵)))
71	70	rspcev 2868	. . . . . . . . 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 1170	. . . . . . . 8 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
76	75, 1	sylibr 134	. . . . . . 7 ⊢ (𝐴 = -∞ → 𝐴 ∈ ℝ^*)
77	76, 29	sylan 283	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
78	55, 74, 77	3jaodan 1317	. . . . 5 ⊢ ((𝐴 = -∞ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
79	2, 78	sylan2b 287	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
80	32, 38, 79	3jaoian 1316	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
81	1, 80	sylanb 284	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
82	81	3impia 1202	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ w3o 979 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ∃wrex 2476 class class class wbr 4034 (class class class)co 5925 ℝcr 7895 1c1 7897 + caddc 7899 +∞cpnf 8075 -∞cmnf 8076 ℝ^*cxr 8077 < clt 8078 − cmin 8214 ℤcz 9343 ℚcq 9710

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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015

This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-id 4329 df-po 4332 df-iso 4333 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-fv 5267 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-n0 9267 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746

This theorem is referenced by: ioo0 10366 ioom 10367 ico0 10368 ioc0 10369 blssps 14747 blss 14748 tgqioo 14875

W3C validator