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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )

Proof

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