qbtwnre - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > qbtwnre		Structured version Visualization version GIF version

Theorem qbtwnre 13215

Description: The rational numbers are dense in ℝ: 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.)

**Assertion**
Ref	Expression
qbtwnre	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

Proof of Theorem qbtwnre Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		posdif 11730	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
2		resubcl 11547	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 − 𝐴) ∈ ℝ)
3		nnrecl 12499	. . . . . . 7 ⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
4	2, 3	sylan 580	. . . . . 6 ⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
5	4	ex 412	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < (𝐵 − 𝐴) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
6	5	ancoms 458	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 − 𝐴) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
7	1, 6	sylbid 240	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
8		nnre 12247	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
9	8	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
10		simplr 768	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐵 ∈ ℝ)
11	9, 10	remulcld 11265	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝐵) ∈ ℝ)
12		peano2rem 11550	. . . . . . 7 ⊢ ((𝑦 · 𝐵) ∈ ℝ → ((𝑦 · 𝐵) − 1) ∈ ℝ)
13	11, 12	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
14		zbtwnre 12962	. . . . . 6 ⊢ (((𝑦 · 𝐵) − 1) ∈ ℝ → ∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
15		reurex 3363	. . . . . 6 ⊢ (∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
16	13, 14, 15	3syl 18	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
17		znq 12968	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑧 / 𝑦) ∈ ℚ)
18	17	ancoms 458	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 / 𝑦) ∈ ℚ)
19	18	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 / 𝑦) ∈ ℚ)
20		an32 646	. . . . . . . . . 10 ⊢ (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ↔ ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
21	8	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℝ)
22		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℝ)
23	21, 22	remulcld 11265	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐴) ∈ ℝ)
24	13	adantrr 717	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
25		zre 12592	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
26	25	ad2antll 729	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑧 ∈ ℝ)
27		ltletr 11327	. . . . . . . . . . . . 13 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ ((𝑦 · 𝐵) − 1) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
28	23, 24, 26, 27	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
29	21	recnd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℂ)
30		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℝ)
31	30	recnd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℂ)
32	22	recnd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℂ)
33	29, 31, 32	subdid 11693	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · (𝐵 − 𝐴)) = ((𝑦 · 𝐵) − (𝑦 · 𝐴)))
34	33	breq2d 5131	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (1 < (𝑦 · (𝐵 − 𝐴)) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
35		1red 11236	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 1 ∈ ℝ)
36	30, 22	resubcld 11665	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝐵 − 𝐴) ∈ ℝ)
37		nngt0 12271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
38	37	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 0 < 𝑦)
39		ltdivmul 12117	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
40	35, 36, 21, 38, 39	syl112anc 1376	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
41	11	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℝ)
42		ltsub13 11718	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ (𝑦 · 𝐵) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
43	23, 41, 35, 42	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
44	34, 40, 43	3bitr4rd 312	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ (1 / 𝑦) < (𝐵 − 𝐴)))
45	44	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ ((1 / 𝑦) < (𝐵 − 𝐴) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧)))
46	45	biancomd 463	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴))))
47		ltmuldiv2 12116	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
48	22, 26, 21, 38, 47	syl112anc 1376	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
49	28, 46, 48	3imtr3d 293	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → 𝐴 < (𝑧 / 𝑦)))
50	41	recnd 11263	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℂ)
51		ax-1cn 11187	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
52		npcan 11491	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
53	50, 51, 52	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
54	53	breq2d 5131	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ 𝑧 < (𝑦 · 𝐵)))
55		ltdivmul 12117	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
56	26, 30, 21, 38, 55	syl112anc 1376	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
57	54, 56	bitr4d 282	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ (𝑧 / 𝑦) < 𝐵))
58	57	biimpd 229	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) → (𝑧 / 𝑦) < 𝐵))
59	49, 58	anim12d 609	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
60	20, 59	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
61		breq2 5123	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝐴 < 𝑥 ↔ 𝐴 < (𝑧 / 𝑦)))
62		breq1 5122	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝑥 < 𝐵 ↔ (𝑧 / 𝑦) < 𝐵))
63	61, 62	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 / 𝑦) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
64	63	rspcev 3601	. . . . . . . . 9 ⊢ (((𝑧 / 𝑦) ∈ ℚ ∧ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
65	19, 60, 64	syl6an 684	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
66	65	expd 415	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
67	66	expr 456	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ ℤ → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))))
68	67	rexlimdv 3139	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
69	16, 68	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
70	69	rexlimdva 3141	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
71	7, 70	syld 47	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
72	71	3impia 1117	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∃wrex 3060 ∃!wreu 3357 class class class wbr 5119 (class class class)co 7405 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 < clt 11269 ≤ cle 11270 − cmin 11466 / cdiv 11894 ℕcn 12240 ℤcz 12588 ℚcq 12964

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-sup 9454 df-inf 9455 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-n0 12502 df-z 12589 df-uz 12853 df-q 12965

This theorem is referenced by: qbtwnxr 13216 qsqueeze 13217 nmoleub2lem3 25066 mbfaddlem 25613 rpnnen3lem 43055

W3C validator