Theorem qbtwnre 4650

Description: The rational numbers are dense in ℝ: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28.

Assertion

Ref	Expression
qbtwnre	⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ A < B) → ∃x ∈ ℚ (A < x ∧ x < B))

Distinct variable group(s):   x,A   x,B

Proof of Theorem qbtwnre

Step	Hyp	Ref	Expression
1		posdift 4365	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B ↔ 0 < (B − A)))
2		nnreclt 4522	. . . . . . 7 ⊢ (((B − A) ∈ ℝ ∧ 0 < (B − A)) → ∃y ∈ ℕ (1 / y) < (B − A))
3		resubclt 4173	. . . . . . 7 ⊢ ((B ∈ ℝ ∧ A ∈ ℝ) → (B − A) ∈ ℝ)
4	2, 3	sylan 343	. . . . . 6 ⊢ (((B ∈ ℝ ∧ A ∈ ℝ) ∧ 0 < (B − A)) → ∃y ∈ ℕ (1 / y) < (B − A))
5	4	exp 291	. . . . 5 ⊢ ((B ∈ ℝ ∧ A ∈ ℝ) → (0 < (B − A) → ∃y ∈ ℕ (1 / y) < (B − A)))
6	5	ancoms 334	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (0 < (B − A) → ∃y ∈ ℕ (1 / y) < (B − A)))
7	1, 6	sylbid 178	. . 3 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B → ∃y ∈ ℕ (1 / y) < (B − A)))
8		axmulrcl 4069	. . . . . . . . . . 11 ⊢ ((y ∈ ℝ ∧ B ∈ ℝ) → (y · B) ∈ ℝ)
9		nnret 4427	. . . . . . . . . . 11 ⊢ (y ∈ ℕ → y ∈ ℝ)
10	8, 9	sylan 343	. . . . . . . . . 10 ⊢ ((y ∈ ℕ ∧ B ∈ ℝ) → (y · B) ∈ ℝ)
11		ax1re 4064	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
12		resubclt 4173	. . . . . . . . . . 11 ⊢ (((y · B) ∈ ℝ ∧ 1 ∈ ℝ) → ((y · B) − 1) ∈ ℝ)
13	11, 12	mpan2 519	. . . . . . . . . 10 ⊢ ((y · B) ∈ ℝ → ((y · B) − 1) ∈ ℝ)
14	10, 13	syl 12	. . . . . . . . 9 ⊢ ((y ∈ ℕ ∧ B ∈ ℝ) → ((y · B) − 1) ∈ ℝ)
15	14	adantrl 311	. . . . . . . 8 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((y · B) − 1) ∈ ℝ)
16		zbtwnre 4619	. . . . . . . 8 ⊢ (((y · B) − 1) ∈ ℝ → ∃!z ∈ ℤ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)))
17		reurex 1337	. . . . . . . 8 ⊢ (∃!z ∈ ℤ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)) → ∃z ∈ ℤ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)))
18	15, 16, 17	3syl 21	. . . . . . 7 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ∃z ∈ ℤ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)))
19		znq 4630	. . . . . . . . . . . . . . . 16 ⊢ ((z ∈ ℤ ∧ y ∈ ℕ) → (z / y) ∈ ℚ)
20	19	ancoms 334	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ ℕ ∧ z ∈ ℤ) → (z / y) ∈ ℚ)
21	20	adantlr 310	. . . . . . . . . . . . . 14 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℤ) → (z / y) ∈ ℚ)
22	21	a1d 14	. . . . . . . . . . . . 13 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℤ) → ((((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ∧ z < (((y · B) − 1) + 1)) → (z / y) ∈ ℚ))
23		subdit 4184	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((y ∈ ℂ ∧ B ∈ ℂ ∧ A ∈ ℂ) → (y · (B − A)) = ((y · B) − (y · A)))
24		nncnt 4428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ ℕ → y ∈ ℂ)
25		recnt 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (B ∈ ℝ → B ∈ ℂ)
26		recnt 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (A ∈ ℝ → A ∈ ℂ)
27	23, 24, 25, 26	syl3an 628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ ℕ ∧ B ∈ ℝ ∧ A ∈ ℝ) → (y · (B − A)) = ((y · B) − (y · A)))
28	27	3com23 616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℕ ∧ A ∈ ℝ ∧ B ∈ ℝ) → (y · (B − A)) = ((y · B) − (y · A)))
29	28	3expb 613	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → (y · (B − A)) = ((y · B) − (y · A)))
30	29	breq2d 2072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → (1 < (y · (B − A)) ↔ 1 < ((y · B) − (y · A))))
31		ltdivmult 4408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ ℝ ∧ y ∈ ℝ ∧ (B − A) ∈ ℝ) → (0 < y → ((1 / y) < (B − A) ↔ 1 < (y · (B − A)))))
32	11, 31	mp3an1 639	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((y ∈ ℝ ∧ (B − A) ∈ ℝ) → (0 < y → ((1 / y) < (B − A) ↔ 1 < (y · (B − A)))))
33	32	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (y ∈ ℝ → ((B − A) ∈ ℝ → (0 < y → ((1 / y) < (B − A) ↔ 1 < (y · (B − A))))))
34	33	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ∈ ℝ → (0 < y → ((B − A) ∈ ℝ → ((1 / y) < (B − A) ↔ 1 < (y · (B − A))))))
35		nngt0t 4441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y ∈ ℕ → 0 < y)
36	34, 9, 35	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y ∈ ℕ → ((B − A) ∈ ℝ → ((1 / y) < (B − A) ↔ 1 < (y · (B − A)))))
37	3	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (B − A) ∈ ℝ)
38	36, 37	syl5 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ ℕ → ((A ∈ ℝ ∧ B ∈ ℝ) → ((1 / y) < (B − A) ↔ 1 < (y · (B − A)))))
39	38	imp 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((1 / y) < (B − A) ↔ 1 < (y · (B − A))))
40		ltsub13t 4360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((y · A) ∈ ℝ ∧ (y · B) ∈ ℝ ∧ 1 ∈ ℝ) → ((y · A) < ((y · B) − 1) ↔ 1 < ((y · B) − (y · A))))
41	11, 40	mp3an3 641	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((y · A) ∈ ℝ ∧ (y · B) ∈ ℝ) → ((y · A) < ((y · B) − 1) ↔ 1 < ((y · B) − (y · A))))
42		axmulrcl 4069	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((y ∈ ℝ ∧ A ∈ ℝ) → (y · A) ∈ ℝ)
43	41, 42, 8	syl2an 349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y ∈ ℝ ∧ A ∈ ℝ) ∧ (y ∈ ℝ ∧ B ∈ ℝ)) → ((y · A) < ((y · B) − 1) ↔ 1 < ((y · B) − (y · A))))
44	43	anandis 394	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℝ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((y · A) < ((y · B) − 1) ↔ 1 < ((y · B) − (y · A))))
45	44, 9	sylan 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((y · A) < ((y · B) − 1) ↔ 1 < ((y · B) − (y · A))))
46	30, 39, 45	3bitr4d 424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((1 / y) < (B − A) ↔ (y · A) < ((y · B) − 1)))
47	46	adantr 306	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → ((1 / y) < (B − A) ↔ (y · A) < ((y · B) − 1)))
48	47	anbi1d 469	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → (((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ↔ ((y · A) < ((y · B) − 1) ∧ ((y · B) − 1) ≤ z)))
49		ltletrt 4290	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y · A) ∈ ℝ ∧ ((y · B) − 1) ∈ ℝ ∧ z ∈ ℝ) → (((y · A) < ((y · B) − 1) ∧ ((y · B) − 1) ≤ z) → (y · A) < z))
50	49	3expa 612	. . . . . . . . . . . . . . . . . 18 ⊢ ((((y · A) ∈ ℝ ∧ ((y · B) − 1) ∈ ℝ) ∧ z ∈ ℝ) → (((y · A) < ((y · B) − 1) ∧ ((y · B) − 1) ≤ z) → (y · A) < z))
51	42, 9	sylan 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℕ ∧ A ∈ ℝ) → (y · A) ∈ ℝ)
52	51	adantrr 312	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → (y · A) ∈ ℝ)
53	52, 15	jca 236	. . . . . . . . . . . . . . . . . 18 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((y · A) ∈ ℝ ∧ ((y · B) − 1) ∈ ℝ))
54	50, 53	sylan 343	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → (((y · A) < ((y · B) − 1) ∧ ((y · B) − 1) ≤ z) → (y · A) < z))
55	48, 54	sylbid 178	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → (((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) → (y · A) < z))
56		ltmuldiv2t 4407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℝ ∧ A ∈ ℝ ∧ z ∈ ℝ) → (0 < y → ((y · A) < z ↔ A < (z / y))))
57	56	3exp 611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ ℝ → (A ∈ ℝ → (z ∈ ℝ → (0 < y → ((y · A) < z ↔ A < (z / y))))))
58	9, 57	syl 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ ℕ → (A ∈ ℝ → (z ∈ ℝ → (0 < y → ((y · A) < z ↔ A < (z / y))))))
59	58	com4r 41	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 < y → (y ∈ ℕ → (A ∈ ℝ → (z ∈ ℝ → ((y · A) < z ↔ A < (z / y))))))
60	35, 59	mpcom 49	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ ℕ → (A ∈ ℝ → (z ∈ ℝ → ((y · A) < z ↔ A < (z / y)))))
61	60	adantrd 308	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ ℕ → ((A ∈ ℝ ∧ B ∈ ℝ) → (z ∈ ℝ → ((y · A) < z ↔ A < (z / y)))))
62	61	imp31 280	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → ((y · A) < z ↔ A < (z / y)))
63	55, 62	sylibd 177	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → (((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) → A < (z / y)))
64		axmulcl 4068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((y ∈ ℂ ∧ B ∈ ℂ) → (y · B) ∈ ℂ)
65	64, 24, 25	syl2an 349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ ℕ ∧ B ∈ ℝ) → (y · B) ∈ ℂ)
66		1cn 4101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
67		npcant 4162	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((y · B) ∈ ℂ ∧ 1 ∈ ℂ) → (((y · B) − 1) + 1) = (y · B))
68	66, 67	mpan2 519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y · B) ∈ ℂ → (((y · B) − 1) + 1) = (y · B))
69	65, 68	syl 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ ℕ ∧ B ∈ ℝ) → (((y · B) − 1) + 1) = (y · B))
70	69	adantr 306	. . . . . . . . . . . . . . . . . . 19 ⊢ (((y ∈ ℕ ∧ B ∈ ℝ) ∧ z ∈ ℝ) → (((y · B) − 1) + 1) = (y · B))
71	70	breq2d 2072	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℕ ∧ B ∈ ℝ) ∧ z ∈ ℝ) → (z < (((y · B) − 1) + 1) ↔ z < (y · B)))
72		3simp2 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((z ∈ ℝ ∧ y ∈ ℕ ∧ B ∈ ℝ) → y ∈ ℕ)
73	72, 35	syl 12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ ℝ ∧ y ∈ ℕ ∧ B ∈ ℝ) → 0 < y)
74		ltdivmult 4408	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((z ∈ ℝ ∧ y ∈ ℝ ∧ B ∈ ℝ) → (0 < y → ((z / y) < B ↔ z < (y · B))))
75	74, 9	syl3an2 620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ ℝ ∧ y ∈ ℕ ∧ B ∈ ℝ) → (0 < y → ((z / y) < B ↔ z < (y · B))))
76	73, 75	mpd 46	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ∈ ℝ ∧ y ∈ ℕ ∧ B ∈ ℝ) → ((z / y) < B ↔ z < (y · B)))
77	76	3coml 617	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ ℕ ∧ B ∈ ℝ ∧ z ∈ ℝ) → ((z / y) < B ↔ z < (y · B)))
78	77	3expa 612	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ ℕ ∧ B ∈ ℝ) ∧ z ∈ ℝ) → ((z / y) < B ↔ z < (y · B)))
79	71, 78	bitr4d 409	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ ℕ ∧ B ∈ ℝ) ∧ z ∈ ℝ) → (z < (((y · B) − 1) + 1) ↔ (z / y) < B))
80	79	biimpd 135	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ ℕ ∧ B ∈ ℝ) ∧ z ∈ ℝ) → (z < (((y · B) − 1) + 1) → (z / y) < B))
81	80	adantlrl 314	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → (z < (((y · B) − 1) + 1) → (z / y) < B))
82	63, 81	anim12d 431	. . . . . . . . . . . . . 14 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℝ) → ((((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ∧ z < (((y · B) − 1) + 1)) → (A < (z / y) ∧ (z / y) < B)))
83		zret 4567	. . . . . . . . . . . . . 14 ⊢ (z ∈ ℤ → z ∈ ℝ)
84	82, 83	sylan2 346	. . . . . . . . . . . . 13 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℤ) → ((((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ∧ z < (((y · B) − 1) + 1)) → (A < (z / y) ∧ (z / y) < B)))
85	22, 84	jcad 455	. . . . . . . . . . . 12 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℤ) → ((((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ∧ z < (((y · B) − 1) + 1)) → ((z / y) ∈ ℚ ∧ (A < (z / y) ∧ (z / y) < B))))
86		breq2 2066	. . . . . . . . . . . . . 14 ⊢ (x = (z / y) → (A < x ↔ A < (z / y)))
87		breq1 2065	. . . . . . . . . . . . . 14 ⊢ (x = (z / y) → (x < B ↔ (z / y) < B))
88	86, 87	anbi12d 476	. . . . . . . . . . . . 13 ⊢ (x = (z / y) → ((A < x ∧ x < B) ↔ (A < (z / y) ∧ (z / y) < B)))
89	88	rcla4ev 1403	. . . . . . . . . . . 12 ⊢ (((z / y) ∈ ℚ ∧ (A < (z / y) ∧ (z / y) < B)) → ∃x ∈ ℚ (A < x ∧ x < B))
90	85, 89	syl6 23	. . . . . . . . . . 11 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℤ) → ((((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ∧ z < (((y · B) − 1) + 1)) → ∃x ∈ ℚ (A < x ∧ x < B)))
91		anass 336	. . . . . . . . . . 11 ⊢ ((((1 / y) < (B − A) ∧ ((y · B) − 1) ≤ z) ∧ z < (((y · B) − 1) + 1)) ↔ ((1 / y) < (B − A) ∧ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1))))
92	90, 91	syl5ibr 182	. . . . . . . . . 10 ⊢ (((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) ∧ z ∈ ℤ) → (((1 / y) < (B − A) ∧ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1))) → ∃x ∈ ℚ (A < x ∧ x < B)))
93	92	exp4b 296	. . . . . . . . 9 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → (z ∈ ℤ → ((1 / y) < (B − A) → ((((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)) → ∃x ∈ ℚ (A < x ∧ x < B)))))
94	93	com34 36	. . . . . . . 8 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → (z ∈ ℤ → ((((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)) → ((1 / y) < (B − A) → ∃x ∈ ℚ (A < x ∧ x < B)))))
95	94	r19.23adv 1286	. . . . . . 7 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → (∃z ∈ ℤ (((y · B) − 1) ≤ z ∧ z < (((y · B) − 1) + 1)) → ((1 / y) < (B − A) → ∃x ∈ ℚ (A < x ∧ x < B))))
96	18, 95	mpd 46	. . . . . 6 ⊢ ((y ∈ ℕ ∧ (A ∈ ℝ ∧ B ∈ ℝ)) → ((1 / y) < (B − A) → ∃x ∈ ℚ (A < x ∧ x < B)))
97	96	ancoms 334	. . . . 5 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ y ∈ ℕ) → ((1 / y) < (B − A) → ∃x ∈ ℚ (A < x ∧ x < B)))
98	97	exp 291	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (y ∈ ℕ → ((1 / y) < (B − A) → ∃x ∈ ℚ (A < x ∧ x < B))))
99	98	r19.23adv 1286	. . 3 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (∃y ∈ ℕ (1 / y) < (B − A) → ∃x ∈ ℚ (A < x ∧ x < B)))
100	7, 99	syld 27	. 2 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B → ∃x ∈ ℚ (A < x ∧ x < B)))
101	100	imp 277	1 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ A < B) → ∃x ∈ ℚ (A < x ∧ x < B))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   ∧ w3a 581   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  ∃!wreu 1203   class class class wbr 2054  (class class class)co 3001  ℂcc 4026  ℝcr 4027  0cc0 4028  1c1 4029   + caddc 4031   · cmulc 4032   < clt 4033   − cmin 4089   / cdiv 4091   ≤ cle 4092  ℕcn 4093  ℤcz 4095  ℚcq 4096

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-ltr 3964  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-r 4038  df-plus 4039  df-mul 4040  df-lt 4041  df-sub 4133  df-neg 4135  df-div 4216  df-le 4277  df-n 4423  df-n0 4535  df-z 4564  df-q 4628

metamath.org