This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )