qbtwnre

Description: The rational numbers are dense in RR : any two real numbers have a rational between them. Exercise 6 of Apostol p. 28. (Contributed by NM, 18-Nov-2004) (Proof shortened by Mario Carneiro, 13-Jun-2014)

		Ref	Expression
	Assertion	qbtwnre	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to \exists x \in ℚ (A < x \land x < B)$

Proof

Step	Hyp	Ref	Expression
1		posdif	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow 0 < B - A)$
2		resubcl	$⊢ (B \in ℝ \land A \in ℝ) \to B - A \in ℝ$
3		nnrecl	$⊢ (B - A \in ℝ \land 0 < B - A) \to \exists y \in ℕ \frac{1}{y} < B - A$
4	2 3	sylan	$⊢ ((B \in ℝ \land A \in ℝ) \land 0 < B - A) \to \exists y \in ℕ \frac{1}{y} < B - A$
5	4	ex	$⊢ (B \in ℝ \land A \in ℝ) \to (0 < B - A \to \exists y \in ℕ \frac{1}{y} < B - A)$
6	5	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < B - A \to \exists y \in ℕ \frac{1}{y} < B - A)$
7	1 6	sylbid	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \to \exists y \in ℕ \frac{1}{y} < B - A)$
8		nnre	$⊢ y \in ℕ \to y \in ℝ$
9	8	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to y \in ℝ$
10		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to B \in ℝ$
11	9 10	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to y B \in ℝ$
12		peano2rem	$⊢ y B \in ℝ \to y B - 1 \in ℝ$
13	11 12	syl	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to y B - 1 \in ℝ$
14		zbtwnre	$⊢ y B - 1 \in ℝ \to \exists! z \in ℤ (y B - 1 \leq z \land z < y B - 1 + 1)$
15		reurex	$⊢ \exists! z \in ℤ (y B - 1 \leq z \land z < y B - 1 + 1) \to \exists z \in ℤ (y B - 1 \leq z \land z < y B - 1 + 1)$
16	13 14 15	3syl	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to \exists z \in ℤ (y B - 1 \leq z \land z < y B - 1 + 1)$
17		znq	$⊢ (z \in ℤ \land y \in ℕ) \to \frac{z}{y} \in ℚ$
18	17	ancoms	$⊢ (y \in ℕ \land z \in ℤ) \to \frac{z}{y} \in ℚ$
19	18	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to \frac{z}{y} \in ℚ$
20		an32	$⊢ ((y B - 1 \leq z \land z < y B - 1 + 1) \land \frac{1}{y} < B - A) \leftrightarrow ((y B - 1 \leq z \land \frac{1}{y} < B - A) \land z < y B - 1 + 1)$
21	8	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y \in ℝ$
22		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to A \in ℝ$
23	21 22	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y A \in ℝ$
24	13	adantrr	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y B - 1 \in ℝ$
25		zre	$⊢ z \in ℤ \to z \in ℝ$
26	25	ad2antll	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to z \in ℝ$
27		ltletr	$⊢ (y A \in ℝ \land y B - 1 \in ℝ \land z \in ℝ) \to ((y A < y B - 1 \land y B - 1 \leq z) \to y A < z)$
28	23 24 26 27	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to ((y A < y B - 1 \land y B - 1 \leq z) \to y A < z)$
29	21	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y \in ℂ$
30		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to B \in ℝ$
31	30	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to B \in ℂ$
32	22	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to A \in ℂ$
33	29 31 32	subdid	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y (B - A) = y B - y A$
34	33	breq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (1 < y (B - A) \leftrightarrow 1 < y B - y A)$
35		1red	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to 1 \in ℝ$
36	30 22	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to B - A \in ℝ$
37		nngt0	$⊢ y \in ℕ \to 0 < y$
38	37	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to 0 < y$
39		ltdivmul	$⊢ (1 \in ℝ \land B - A \in ℝ \land (y \in ℝ \land 0 < y)) \to (\frac{1}{y} < B - A \leftrightarrow 1 < y (B - A))$
40	35 36 21 38 39	syl112anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (\frac{1}{y} < B - A \leftrightarrow 1 < y (B - A))$
41	11	adantrr	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y B \in ℝ$
42		ltsub13	$⊢ (y A \in ℝ \land y B \in ℝ \land 1 \in ℝ) \to (y A < y B - 1 \leftrightarrow 1 < y B - y A)$
43	23 41 35 42	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (y A < y B - 1 \leftrightarrow 1 < y B - y A)$
44	34 40 43	3bitr4rd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (y A < y B - 1 \leftrightarrow \frac{1}{y} < B - A)$
45	44	anbi1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to ((y A < y B - 1 \land y B - 1 \leq z) \leftrightarrow (\frac{1}{y} < B - A \land y B - 1 \leq z))$
46	45	biancomd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to ((y A < y B - 1 \land y B - 1 \leq z) \leftrightarrow (y B - 1 \leq z \land \frac{1}{y} < B - A))$
47		ltmuldiv2	$⊢ (A \in ℝ \land z \in ℝ \land (y \in ℝ \land 0 < y)) \to (y A < z \leftrightarrow A < \frac{z}{y})$
48	22 26 21 38 47	syl112anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (y A < z \leftrightarrow A < \frac{z}{y})$
49	28 46 48	3imtr3d	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to ((y B - 1 \leq z \land \frac{1}{y} < B - A) \to A < \frac{z}{y})$
50	41	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y B \in ℂ$
51		ax-1cn	$⊢ 1 \in ℂ$
52		npcan	$⊢ (y B \in ℂ \land 1 \in ℂ) \to y B - 1 + 1 = y B$
53	50 51 52	sylancl	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to y B - 1 + 1 = y B$
54	53	breq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (z < y B - 1 + 1 \leftrightarrow z < y B)$
55		ltdivmul	$⊢ (z \in ℝ \land B \in ℝ \land (y \in ℝ \land 0 < y)) \to (\frac{z}{y} < B \leftrightarrow z < y B)$
56	26 30 21 38 55	syl112anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (\frac{z}{y} < B \leftrightarrow z < y B)$
57	54 56	bitr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (z < y B - 1 + 1 \leftrightarrow \frac{z}{y} < B)$
58	57	biimpd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (z < y B - 1 + 1 \to \frac{z}{y} < B)$
59	49 58	anim12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (((y B - 1 \leq z \land \frac{1}{y} < B - A) \land z < y B - 1 + 1) \to (A < \frac{z}{y} \land \frac{z}{y} < B))$
60	20 59	syl5bi	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (((y B - 1 \leq z \land z < y B - 1 + 1) \land \frac{1}{y} < B - A) \to (A < \frac{z}{y} \land \frac{z}{y} < B))$
61		breq2	$⊢ x = \frac{z}{y} \to (A < x \leftrightarrow A < \frac{z}{y})$
62		breq1	$⊢ x = \frac{z}{y} \to (x < B \leftrightarrow \frac{z}{y} < B)$
63	61 62	anbi12d	$⊢ x = \frac{z}{y} \to ((A < x \land x < B) \leftrightarrow (A < \frac{z}{y} \land \frac{z}{y} < B))$
64	63	rspcev	$⊢ (\frac{z}{y} \in ℚ \land (A < \frac{z}{y} \land \frac{z}{y} < B)) \to \exists x \in ℚ (A < x \land x < B)$
65	19 60 64	syl6an	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to (((y B - 1 \leq z \land z < y B - 1 + 1) \land \frac{1}{y} < B - A) \to \exists x \in ℚ (A < x \land x < B))$
66	65	expd	$⊢ ((A \in ℝ \land B \in ℝ) \land (y \in ℕ \land z \in ℤ)) \to ((y B - 1 \leq z \land z < y B - 1 + 1) \to (\frac{1}{y} < B - A \to \exists x \in ℚ (A < x \land x < B)))$
67	66	expr	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to (z \in ℤ \to ((y B - 1 \leq z \land z < y B - 1 + 1) \to (\frac{1}{y} < B - A \to \exists x \in ℚ (A < x \land x < B))))$
68	67	rexlimdv	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to (\exists z \in ℤ (y B - 1 \leq z \land z < y B - 1 + 1) \to (\frac{1}{y} < B - A \to \exists x \in ℚ (A < x \land x < B)))$
69	16 68	mpd	$⊢ ((A \in ℝ \land B \in ℝ) \land y \in ℕ) \to (\frac{1}{y} < B - A \to \exists x \in ℚ (A < x \land x < B))$
70	69	rexlimdva	$⊢ (A \in ℝ \land B \in ℝ) \to (\exists y \in ℕ \frac{1}{y} < B - A \to \exists x \in ℚ (A < x \land x < B))$
71	7 70	syld	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \to \exists x \in ℚ (A < x \land x < B))$
72	71	3impia	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to \exists x \in ℚ (A < x \land x < B)$

Metamath Proof Explorer

Theorem qbtwnre

Proof