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	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℚ (A < x \land x < B)$

Proof

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

Metamath Proof Explorer

Theorem qbtwnxr

Proof