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 12633

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 11171	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
2		resubcl 10988	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 − 𝐴) ∈ ℝ)
3		nnrecl 11932	. . . . . . 7 ⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
4	2, 3	sylan 583	. . . . . 6 ⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
5	4	ex 416	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < (𝐵 − 𝐴) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
6	5	ancoms 462	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 − 𝐴) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
7	1, 6	sylbid 243	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
8		nnre 11681	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
9	8	adantl 485	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
10		simplr 768	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐵 ∈ ℝ)
11	9, 10	remulcld 10709	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝐵) ∈ ℝ)
12		peano2rem 10991	. . . . . . 7 ⊢ ((𝑦 · 𝐵) ∈ ℝ → ((𝑦 · 𝐵) − 1) ∈ ℝ)
13	11, 12	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
14		zbtwnre 12386	. . . . . 6 ⊢ (((𝑦 · 𝐵) − 1) ∈ ℝ → ∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
15		reurex 3341	. . . . . 6 ⊢ (∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
16	13, 14, 15	3syl 18	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
17		znq 12392	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑧 / 𝑦) ∈ ℚ)
18	17	ancoms 462	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 / 𝑦) ∈ ℚ)
19	18	adantl 485	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 / 𝑦) ∈ ℚ)
20		an32 645	. . . . . . . . . 10 ⊢ (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ↔ ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
21	8	ad2antrl 727	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℝ)
22		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℝ)
23	21, 22	remulcld 10709	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐴) ∈ ℝ)
24	13	adantrr 716	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
25		zre 12024	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
26	25	ad2antll 728	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑧 ∈ ℝ)
27		ltletr 10770	. . . . . . . . . . . . 13 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ ((𝑦 · 𝐵) − 1) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
28	23, 24, 26, 27	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
29	21	recnd 10707	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℂ)
30		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℝ)
31	30	recnd 10707	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℂ)
32	22	recnd 10707	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℂ)
33	29, 31, 32	subdid 11134	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · (𝐵 − 𝐴)) = ((𝑦 · 𝐵) − (𝑦 · 𝐴)))
34	33	breq2d 5044	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (1 < (𝑦 · (𝐵 − 𝐴)) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
35		1red 10680	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 1 ∈ ℝ)
36	30, 22	resubcld 11106	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝐵 − 𝐴) ∈ ℝ)
37		nngt0 11705	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
38	37	ad2antrl 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 0 < 𝑦)
39		ltdivmul 11553	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
40	35, 36, 21, 38, 39	syl112anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
41	11	adantrr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℝ)
42		ltsub13 11159	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ (𝑦 · 𝐵) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
43	23, 41, 35, 42	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
44	34, 40, 43	3bitr4rd 315	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ (1 / 𝑦) < (𝐵 − 𝐴)))
45	44	anbi1d 632	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ ((1 / 𝑦) < (𝐵 − 𝐴) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧)))
46	45	biancomd 467	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴))))
47		ltmuldiv2 11552	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
48	22, 26, 21, 38, 47	syl112anc 1371	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
49	28, 46, 48	3imtr3d 296	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → 𝐴 < (𝑧 / 𝑦)))
50	41	recnd 10707	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℂ)
51		ax-1cn 10633	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
52		npcan 10933	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
53	50, 51, 52	sylancl 589	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
54	53	breq2d 5044	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ 𝑧 < (𝑦 · 𝐵)))
55		ltdivmul 11553	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
56	26, 30, 21, 38, 55	syl112anc 1371	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
57	54, 56	bitr4d 285	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ (𝑧 / 𝑦) < 𝐵))
58	57	biimpd 232	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) → (𝑧 / 𝑦) < 𝐵))
59	49, 58	anim12d 611	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
60	20, 59	syl5bi 245	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
61		breq2 5036	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝐴 < 𝑥 ↔ 𝐴 < (𝑧 / 𝑦)))
62		breq1 5035	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝑥 < 𝐵 ↔ (𝑧 / 𝑦) < 𝐵))
63	61, 62	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 / 𝑦) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
64	63	rspcev 3541	. . . . . . . . 9 ⊢ (((𝑧 / 𝑦) ∈ ℚ ∧ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
65	19, 60, 64	syl6an 683	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
66	65	expd 419	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
67	66	expr 460	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ ℤ → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))))
68	67	rexlimdv 3207	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
69	16, 68	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
70	69	rexlimdva 3208	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
71	7, 70	syld 47	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
72	71	3impia 1114	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∃wrex 3071 ∃!wreu 3072 class class class wbr 5032 (class class class)co 7150 ℂcc 10573 ℝcr 10574 0cc0 10575 1c1 10576 + caddc 10578 · cmul 10580 < clt 10713 ≤ cle 10714 − cmin 10908 / cdiv 11335 ℕcn 11674 ℤcz 12020 ℚcq 12388

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-iun 4885 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-1st 7693 df-2nd 7694 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-er 8299 df-en 8528 df-dom 8529 df-sdom 8530 df-sup 8939 df-inf 8940 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-div 11336 df-nn 11675 df-n0 11935 df-z 12021 df-uz 12283 df-q 12389

This theorem is referenced by: qbtwnxr 12634 qsqueeze 12635 nmoleub2lem3 23816 mbfaddlem 24360 rpnnen3lem 40345

W3C validator