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 13118

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 11634	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
2		resubcl 11449	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 − 𝐴) ∈ ℝ)
3		nnrecl 12403	. . . . . . 7 ⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
4	2, 3	sylan 581	. . . . . 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 12156	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
9	8	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
10		simplr 769	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐵 ∈ ℝ)
11	9, 10	remulcld 11166	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝐵) ∈ ℝ)
12		peano2rem 11452	. . . . . . 7 ⊢ ((𝑦 · 𝐵) ∈ ℝ → ((𝑦 · 𝐵) − 1) ∈ ℝ)
13	11, 12	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
14		zbtwnre 12863	. . . . . 6 ⊢ (((𝑦 · 𝐵) − 1) ∈ ℝ → ∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
15		reurex 3355	. . . . . 6 ⊢ (∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
16	13, 14, 15	3syl 18	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
17		znq 12869	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑧 / 𝑦) ∈ ℚ)
18	17	ancoms 458	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 / 𝑦) ∈ ℚ)
19	18	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 / 𝑦) ∈ ℚ)
20		an32 647	. . . . . . . . . 10 ⊢ (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ↔ ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
21	8	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℝ)
22		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℝ)
23	21, 22	remulcld 11166	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐴) ∈ ℝ)
24	13	adantrr 718	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
25		zre 12496	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
26	25	ad2antll 730	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑧 ∈ ℝ)
27		ltletr 11229	. . . . . . . . . . . . 13 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ ((𝑦 · 𝐵) − 1) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
28	23, 24, 26, 27	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
29	21	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℂ)
30		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℝ)
31	30	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℂ)
32	22	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℂ)
33	29, 31, 32	subdid 11597	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · (𝐵 − 𝐴)) = ((𝑦 · 𝐵) − (𝑦 · 𝐴)))
34	33	breq2d 5111	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (1 < (𝑦 · (𝐵 − 𝐴)) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
35		1red 11137	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 1 ∈ ℝ)
36	30, 22	resubcld 11569	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝐵 − 𝐴) ∈ ℝ)
37		nngt0 12180	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
38	37	ad2antrl 729	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 0 < 𝑦)
39		ltdivmul 12021	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
40	35, 36, 21, 38, 39	syl112anc 1377	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
41	11	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℝ)
42		ltsub13 11622	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ (𝑦 · 𝐵) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
43	23, 41, 35, 42	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
44	34, 40, 43	3bitr4rd 312	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ (1 / 𝑦) < (𝐵 − 𝐴)))
45	44	anbi1d 632	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ ((1 / 𝑦) < (𝐵 − 𝐴) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧)))
46	45	biancomd 463	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴))))
47		ltmuldiv2 12020	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
48	22, 26, 21, 38, 47	syl112anc 1377	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
49	28, 46, 48	3imtr3d 293	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → 𝐴 < (𝑧 / 𝑦)))
50	41	recnd 11164	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℂ)
51		ax-1cn 11088	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
52		npcan 11393	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
53	50, 51, 52	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
54	53	breq2d 5111	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ 𝑧 < (𝑦 · 𝐵)))
55		ltdivmul 12021	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
56	26, 30, 21, 38, 55	syl112anc 1377	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
57	54, 56	bitr4d 282	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ (𝑧 / 𝑦) < 𝐵))
58	57	biimpd 229	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) → (𝑧 / 𝑦) < 𝐵))
59	49, 58	anim12d 610	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
60	20, 59	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
61		breq2 5103	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝐴 < 𝑥 ↔ 𝐴 < (𝑧 / 𝑦)))
62		breq1 5102	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝑥 < 𝐵 ↔ (𝑧 / 𝑦) < 𝐵))
63	61, 62	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 / 𝑦) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
64	63	rspcev 3577	. . . . . . . . 9 ⊢ (((𝑧 / 𝑦) ∈ ℚ ∧ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
65	19, 60, 64	syl6an 685	. . . . . . . 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 3136	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
69	16, 68	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
70	69	rexlimdva 3138	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
71	7, 70	syld 47	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
72	71	3impia 1118	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃wrex 3061 ∃!wreu 3349 class class class wbr 5099 (class class class)co 7360 ℂcc 11028 ℝcr 11029 0cc0 11030 1c1 11031 + caddc 11033 · cmul 11035 < clt 11170 ≤ cle 11171 − cmin 11368 / cdiv 11798 ℕcn 12149 ℤcz 12492 ℚcq 12865

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4949 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-sup 9349 df-inf 9350 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12150 df-n0 12406 df-z 12493 df-uz 12756 df-q 12866

This theorem is referenced by: qbtwnxr 13119 qsqueeze 13120 nmoleub2lem3 25075 mbfaddlem 25621 rpnnen3lem 43340

W3C validator