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 12593

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 11133	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
2		resubcl 10950	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 − 𝐴) ∈ ℝ)
3		nnrecl 11896	. . . . . . 7 ⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
4	2, 3	sylan 582	. . . . . 6 ⊢ (((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ 0 < (𝐵 − 𝐴)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴))
5	4	ex 415	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < (𝐵 − 𝐴) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
6	5	ancoms 461	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 − 𝐴) → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
7	1, 6	sylbid 242	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴)))
8		nnre 11645	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
9	8	adantl 484	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
10		simplr 767	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → 𝐵 ∈ ℝ)
11	9, 10	remulcld 10671	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝐵) ∈ ℝ)
12		peano2rem 10953	. . . . . . 7 ⊢ ((𝑦 · 𝐵) ∈ ℝ → ((𝑦 · 𝐵) − 1) ∈ ℝ)
13	11, 12	syl 17	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
14		zbtwnre 12347	. . . . . 6 ⊢ (((𝑦 · 𝐵) − 1) ∈ ℝ → ∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
15		reurex 3431	. . . . . 6 ⊢ (∃!𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
16	13, 14, 15	3syl 18	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
17		znq 12353	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑧 / 𝑦) ∈ ℚ)
18	17	ancoms 461	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 / 𝑦) ∈ ℚ)
19	18	adantl 484	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 / 𝑦) ∈ ℚ)
20		an32 644	. . . . . . . . . 10 ⊢ (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ↔ ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)))
21	8	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℝ)
22		simpll 765	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℝ)
23	21, 22	remulcld 10671	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐴) ∈ ℝ)
24	13	adantrr 715	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐵) − 1) ∈ ℝ)
25		zre 11986	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
26	25	ad2antll 727	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑧 ∈ ℝ)
27		ltletr 10732	. . . . . . . . . . . . 13 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ ((𝑦 · 𝐵) − 1) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
28	23, 24, 26, 27	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) → (𝑦 · 𝐴) < 𝑧))
29	21	recnd 10669	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝑦 ∈ ℂ)
30		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℝ)
31	30	recnd 10669	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐵 ∈ ℂ)
32	22	recnd 10669	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 𝐴 ∈ ℂ)
33	29, 31, 32	subdid 11096	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · (𝐵 − 𝐴)) = ((𝑦 · 𝐵) − (𝑦 · 𝐴)))
34	33	breq2d 5078	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (1 < (𝑦 · (𝐵 − 𝐴)) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
35		1red 10642	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 1 ∈ ℝ)
36	30, 22	resubcld 11068	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝐵 − 𝐴) ∈ ℝ)
37		nngt0 11669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
38	37	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → 0 < 𝑦)
39		ltdivmul 11515	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
40	35, 36, 21, 38, 39	syl112anc 1370	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((1 / 𝑦) < (𝐵 − 𝐴) ↔ 1 < (𝑦 · (𝐵 − 𝐴))))
41	11	adantrr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℝ)
42		ltsub13 11121	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 · 𝐴) ∈ ℝ ∧ (𝑦 · 𝐵) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
43	23, 41, 35, 42	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ 1 < ((𝑦 · 𝐵) − (𝑦 · 𝐴))))
44	34, 40, 43	3bitr4rd 314	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ↔ (1 / 𝑦) < (𝐵 − 𝐴)))
45	44	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ ((1 / 𝑦) < (𝐵 − 𝐴) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧)))
46	45	biancomd 466	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐴) < ((𝑦 · 𝐵) − 1) ∧ ((𝑦 · 𝐵) − 1) ≤ 𝑧) ↔ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴))))
47		ltmuldiv2 11514	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
48	22, 26, 21, 38, 47	syl112anc 1370	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑦 · 𝐴) < 𝑧 ↔ 𝐴 < (𝑧 / 𝑦)))
49	28, 46, 48	3imtr3d 295	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → 𝐴 < (𝑧 / 𝑦)))
50	41	recnd 10669	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑦 · 𝐵) ∈ ℂ)
51		ax-1cn 10595	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
52		npcan 10895	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
53	50, 51, 52	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((𝑦 · 𝐵) − 1) + 1) = (𝑦 · 𝐵))
54	53	breq2d 5078	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ 𝑧 < (𝑦 · 𝐵)))
55		ltdivmul 11515	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 0 < 𝑦)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
56	26, 30, 21, 38, 55	syl112anc 1370	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((𝑧 / 𝑦) < 𝐵 ↔ 𝑧 < (𝑦 · 𝐵)))
57	54, 56	bitr4d 284	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) ↔ (𝑧 / 𝑦) < 𝐵))
58	57	biimpd 231	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (𝑧 < (((𝑦 · 𝐵) − 1) + 1) → (𝑧 / 𝑦) < 𝐵))
59	49, 58	anim12d 610	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ (1 / 𝑦) < (𝐵 − 𝐴)) ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
60	20, 59	syl5bi 244	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
61		breq2 5070	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝐴 < 𝑥 ↔ 𝐴 < (𝑧 / 𝑦)))
62		breq1 5069	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑧 / 𝑦) → (𝑥 < 𝐵 ↔ (𝑧 / 𝑦) < 𝐵))
63	61, 62	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = (𝑧 / 𝑦) → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)))
64	63	rspcev 3623	. . . . . . . . 9 ⊢ (((𝑧 / 𝑦) ∈ ℚ ∧ (𝐴 < (𝑧 / 𝑦) ∧ (𝑧 / 𝑦) < 𝐵)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
65	19, 60, 64	syl6an 682	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → (((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) ∧ (1 / 𝑦) < (𝐵 − 𝐴)) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
66	65	expd 418	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ)) → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
67	66	expr 459	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (𝑧 ∈ ℤ → ((((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))))
68	67	rexlimdv 3283	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → (∃𝑧 ∈ ℤ (((𝑦 · 𝐵) − 1) ≤ 𝑧 ∧ 𝑧 < (((𝑦 · 𝐵) − 1) + 1)) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))))
69	16, 68	mpd 15	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑦 ∈ ℕ) → ((1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
70	69	rexlimdva 3284	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑦 ∈ ℕ (1 / 𝑦) < (𝐵 − 𝐴) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
71	7, 70	syld 47	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)))
72	71	3impia 1113	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∃wrex 3139 ∃!wreu 3140 class class class wbr 5066 (class class class)co 7156 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 < clt 10675 ≤ cle 10676 − cmin 10870 / cdiv 11297 ℕcn 11638 ℤcz 11982 ℚcq 12349

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-sup 8906 df-inf 8907 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-n0 11899 df-z 11983 df-uz 12245 df-q 12350

This theorem is referenced by: qbtwnxr 12594 qsqueeze 12595 nmoleub2lem3 23719 mbfaddlem 24261 rpnnen3lem 39648

W3C validator