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

Metamath Proof Explorer

Theorem qbtwnxr

Description: The rational numbers are dense in RR* : any two extended real numbers have a rational between them. (Contributed by NM, 6-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion qbtwnxr ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elxr ⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2 elxr ⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
3 qbtwnre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
4 3 3expia ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
5 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → 𝐴 ∈ ℝ )
6 peano2re ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
7 6 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐴 + 1 ) ∈ ℝ )
8 ltp1 ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( 𝐴 + 1 ) )
9 8 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → 𝐴 < ( 𝐴 + 1 ) )
10 qbtwnre ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ∧ 𝐴 < ( 𝐴 + 1 ) ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) )
11 5 7 9 10 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) )
12 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
13 12 ltpnfd ⊢ ( 𝑥 ∈ ℚ → 𝑥 < +∞ )
14 13 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∧ 𝑥 ∈ ℚ ) → 𝑥 < +∞ )
15 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∧ 𝑥 ∈ ℚ ) → 𝐵 = +∞ )
16 14 15 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∧ 𝑥 ∈ ℚ ) → 𝑥 < 𝐵 )
17 16 a1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∧ 𝑥 ∈ ℚ ) → ( 𝑥 < ( 𝐴 + 1 ) → 𝑥 < 𝐵 ) )
18 17 anim2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∧ 𝑥 ∈ ℚ ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) → ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
19 18 reximdva ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
20 11 19 mpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
21 20 a1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
22 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
23 breq2 ⊢ ( 𝐵 = -∞ → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
24 23 adantl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
25 nltmnf ⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )
26 25 adantr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 = -∞ ) → ¬ 𝐴 < -∞ )
27 26 pm2.21d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( 𝐴 < -∞ → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
28 24 27 sylbid ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
29 22 28 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
30 4 21 29 3jaodan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
31 2 30 sylan2b ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
32 breq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
33 32 adantr ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
34 pnfnlt ⊢ ( 𝐵 ∈ ℝ* → ¬ +∞ < 𝐵 )
35 34 adantl ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ +∞ < 𝐵 )
36 35 pm2.21d ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( +∞ < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
37 33 36 sylbid ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
38 peano2rem ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
39 38 adantl ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 − 1 ) ∈ ℝ )
40 simpr ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
41 ltm1 ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) < 𝐵 )
42 41 adantl ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 − 1 ) < 𝐵 )
43 qbtwnre ⊢ ( ( ( 𝐵 − 1 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐵 − 1 ) < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( ( 𝐵 − 1 ) < 𝑥 ∧ 𝑥 < 𝐵 ) )
44 39 40 42 43 syl3anc ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℚ ( ( 𝐵 − 1 ) < 𝑥 ∧ 𝑥 < 𝐵 ) )
45 simpll ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℚ ) → 𝐴 = -∞ )
46 12 adantl ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℚ ) → 𝑥 ∈ ℝ )
47 46 mnfltd ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℚ ) → -∞ < 𝑥 )
48 45 47 eqbrtrd ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℚ ) → 𝐴 < 𝑥 )
49 48 a1d ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℚ ) → ( ( 𝐵 − 1 ) < 𝑥 → 𝐴 < 𝑥 ) )
50 49 anim1d ⊢ ( ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℚ ) → ( ( ( 𝐵 − 1 ) < 𝑥 ∧ 𝑥 < 𝐵 ) → ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
51 50 reximdva ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℚ ( ( 𝐵 − 1 ) < 𝑥 ∧ 𝑥 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
52 44 51 mpd ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
53 52 a1d ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
54 1re ⊢ 1 ∈ ℝ
55 mnflt ⊢ ( 1 ∈ ℝ → -∞ < 1 )
56 54 55 ax-mp ⊢ -∞ < 1
57 breq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 < 1 ↔ -∞ < 1 ) )
58 56 57 mpbiri ⊢ ( 𝐴 = -∞ → 𝐴 < 1 )
59 ltpnf ⊢ ( 1 ∈ ℝ → 1 < +∞ )
60 54 59 ax-mp ⊢ 1 < +∞
61 breq2 ⊢ ( 𝐵 = +∞ → ( 1 < 𝐵 ↔ 1 < +∞ ) )
62 60 61 mpbiri ⊢ ( 𝐵 = +∞ → 1 < 𝐵 )
63 1z ⊢ 1 ∈ ℤ
64 zq ⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
65 63 64 ax-mp ⊢ 1 ∈ ℚ
66 breq2 ⊢ ( 𝑥 = 1 → ( 𝐴 < 𝑥 ↔ 𝐴 < 1 ) )
67 breq1 ⊢ ( 𝑥 = 1 → ( 𝑥 < 𝐵 ↔ 1 < 𝐵 ) )
68 66 67 anbi12d ⊢ ( 𝑥 = 1 → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ↔ ( 𝐴 < 1 ∧ 1 < 𝐵 ) ) )
69 68 rspcev ⊢ ( ( 1 ∈ ℚ ∧ ( 𝐴 < 1 ∧ 1 < 𝐵 ) ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
70 65 69 mpan ⊢ ( ( 𝐴 < 1 ∧ 1 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
71 58 62 70 syl2an ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
72 71 a1d ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
73 3mix3 ⊢ ( 𝐴 = -∞ → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
74 73 1 sylibr ⊢ ( 𝐴 = -∞ → 𝐴 ∈ ℝ* )
75 74 28 sylan ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
76 53 72 75 3jaodan ⊢ ( ( 𝐴 = -∞ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
77 2 76 sylan2b ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
78 31 37 77 3jaoian ⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
79 1 78 sylanb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
80 79 3impia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )