Theorem qbtwnre

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

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

Proof

Step	Hyp	Ref	Expression
1		posdif	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
2		resubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
3		nnrecl	⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ 0 < ( 𝐵 − 𝐴 ) ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) )
4	2 3	sylan	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 0 < ( 𝐵 − 𝐴 ) ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) )
5	4	ex	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < ( 𝐵 − 𝐴 ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) )
6	5	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < ( 𝐵 − 𝐴 ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) )
7	1 6	sylbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) )
8		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
9	8	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℝ )
10		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → 𝐵 ∈ ℝ )
11	9 10	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 · 𝐵 ) ∈ ℝ )
12		peano2rem	⊢ ( ( 𝑦 · 𝐵 ) ∈ ℝ → ( ( 𝑦 · 𝐵 ) − 1 ) ∈ ℝ )
13	11 12	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝐵 ) − 1 ) ∈ ℝ )
14		zbtwnre	⊢ ( ( ( 𝑦 · 𝐵 ) − 1 ) ∈ ℝ → ∃! 𝑧 ∈ ℤ ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) )
15		reurex	⊢ ( ∃! 𝑧 ∈ ℤ ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) → ∃ 𝑧 ∈ ℤ ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) )
16	13 14 15	3syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ∃ 𝑧 ∈ ℤ ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) )
17		znq	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑧 / 𝑦 ) ∈ ℚ )
18	17	ancoms	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 / 𝑦 ) ∈ ℚ )
19	18	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑧 / 𝑦 ) ∈ ℚ )
20		an32	⊢ ( ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) ↔ ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) )
21	8	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝑦 ∈ ℝ )
22		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝐴 ∈ ℝ )
23	21 22	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 · 𝐴 ) ∈ ℝ )
24	13	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 · 𝐵 ) − 1 ) ∈ ℝ )
25		zre	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
26	25	ad2antll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝑧 ∈ ℝ )
27		ltletr	⊢ ( ( ( 𝑦 · 𝐴 ) ∈ ℝ ∧ ( ( 𝑦 · 𝐵 ) − 1 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ∧ ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ) → ( 𝑦 · 𝐴 ) < 𝑧 ) )
28	23 24 26 27	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ∧ ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ) → ( 𝑦 · 𝐴 ) < 𝑧 ) )
29	21	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝑦 ∈ ℂ )
30		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝐵 ∈ ℝ )
31	30	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
32	22	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
33	29 31 32	subdid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 · ( 𝐵 − 𝐴 ) ) = ( ( 𝑦 · 𝐵 ) − ( 𝑦 · 𝐴 ) ) )
34	33	breq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 1 < ( 𝑦 · ( 𝐵 − 𝐴 ) ) ↔ 1 < ( ( 𝑦 · 𝐵 ) − ( 𝑦 · 𝐴 ) ) ) )
35		1red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 1 ∈ ℝ )
36	30 22	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
37		nngt0	⊢ ( 𝑦 ∈ ℕ → 0 < 𝑦 )
38	37	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → 0 < 𝑦 )
39		ltdivmul	⊢ ( ( 1 ∈ ℝ ∧ ( 𝐵 − 𝐴 ) ∈ ℝ ∧ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) → ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ↔ 1 < ( 𝑦 · ( 𝐵 − 𝐴 ) ) ) )
40	35 36 21 38 39	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ↔ 1 < ( 𝑦 · ( 𝐵 − 𝐴 ) ) ) )
41	11	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 · 𝐵 ) ∈ ℝ )
42		ltsub13	⊢ ( ( ( 𝑦 · 𝐴 ) ∈ ℝ ∧ ( 𝑦 · 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ↔ 1 < ( ( 𝑦 · 𝐵 ) − ( 𝑦 · 𝐴 ) ) ) )
43	23 41 35 42	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ↔ 1 < ( ( 𝑦 · 𝐵 ) − ( 𝑦 · 𝐴 ) ) ) )
44	34 40 43	3bitr4rd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ↔ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) )
45	44	anbi1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ∧ ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ) ↔ ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ∧ ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ) ) )
46	45	biancomd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( 𝑦 · 𝐴 ) < ( ( 𝑦 · 𝐵 ) − 1 ) ∧ ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ) ↔ ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) ) )
47		ltmuldiv2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) → ( ( 𝑦 · 𝐴 ) < 𝑧 ↔ 𝐴 < ( 𝑧 / 𝑦 ) ) )
48	22 26 21 38 47	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 · 𝐴 ) < 𝑧 ↔ 𝐴 < ( 𝑧 / 𝑦 ) ) )
49	28 46 48	3imtr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) → 𝐴 < ( 𝑧 / 𝑦 ) ) )
50	41	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 · 𝐵 ) ∈ ℂ )
51		ax-1cn	⊢ 1 ∈ ℂ
52		npcan	⊢ ( ( ( 𝑦 · 𝐵 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) = ( 𝑦 · 𝐵 ) )
53	50 51 52	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) = ( 𝑦 · 𝐵 ) )
54	53	breq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ↔ 𝑧 < ( 𝑦 · 𝐵 ) ) )
55		ltdivmul	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) → ( ( 𝑧 / 𝑦 ) < 𝐵 ↔ 𝑧 < ( 𝑦 · 𝐵 ) ) )
56	26 30 21 38 55	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑧 / 𝑦 ) < 𝐵 ↔ 𝑧 < ( 𝑦 · 𝐵 ) ) )
57	54 56	bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ↔ ( 𝑧 / 𝑦 ) < 𝐵 ) )
58	57	biimpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) → ( 𝑧 / 𝑦 ) < 𝐵 ) )
59	49 58	anim12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) → ( 𝐴 < ( 𝑧 / 𝑦 ) ∧ ( 𝑧 / 𝑦 ) < 𝐵 ) ) )
60	20 59	biimtrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) → ( 𝐴 < ( 𝑧 / 𝑦 ) ∧ ( 𝑧 / 𝑦 ) < 𝐵 ) ) )
61		breq2	⊢ ( 𝑥 = ( 𝑧 / 𝑦 ) → ( 𝐴 < 𝑥 ↔ 𝐴 < ( 𝑧 / 𝑦 ) ) )
62		breq1	⊢ ( 𝑥 = ( 𝑧 / 𝑦 ) → ( 𝑥 < 𝐵 ↔ ( 𝑧 / 𝑦 ) < 𝐵 ) )
63	61 62	anbi12d	⊢ ( 𝑥 = ( 𝑧 / 𝑦 ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ↔ ( 𝐴 < ( 𝑧 / 𝑦 ) ∧ ( 𝑧 / 𝑦 ) < 𝐵 ) ) )
64	63	rspcev	⊢ ( ( ( 𝑧 / 𝑦 ) ∈ ℚ ∧ ( 𝐴 < ( 𝑧 / 𝑦 ) ∧ ( 𝑧 / 𝑦 ) < 𝐵 ) ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
65	19 60 64	syl6an	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) ∧ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
66	65	expd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) → ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) ) )
67	66	expr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( 𝑧 ∈ ℤ → ( ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) → ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) ) ) )
68	67	rexlimdv	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ∃ 𝑧 ∈ ℤ ( ( ( 𝑦 · 𝐵 ) − 1 ) ≤ 𝑧 ∧ 𝑧 < ( ( ( 𝑦 · 𝐵 ) − 1 ) + 1 ) ) → ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) ) )
69	16 68	mpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑦 ∈ ℕ ) → ( ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
70	69	rexlimdva	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < ( 𝐵 − 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
71	7 70	syld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
72	71	3impia	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )