Metamath Proof Explorer

Theorem qinioo

Description: The rational numbers are dense in RR . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses qinioo.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
qinioo.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
Assertion qinioo ( 𝜑 → ( ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 qinioo.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 qinioo.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 simplr ⊢ ( ( ( 𝜑 ∧ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
4 1 2 xrltnled ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
5 4 biimpar ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐴 ) → 𝐴 < 𝐵 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
8 simpr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
9 qbtwnxr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑞 ∈ ℚ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) )
10 6 7 8 9 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ∃ 𝑞 ∈ ℚ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) )
11 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝐴 ∈ ℝ* )
12 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝐵 ∈ ℝ* )
13 qre ⊢ ( 𝑞 ∈ ℚ → 𝑞 ∈ ℝ )
14 13 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝑞 ∈ ℝ )
15 simprl ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝐴 < 𝑞 )
16 simprr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝑞 < 𝐵 )
17 11 12 14 15 16 eliood ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝑞 ∈ ( 𝐴 (,) 𝐵 ) )
18 17 ex ⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) → ( ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) → 𝑞 ∈ ( 𝐴 (,) 𝐵 ) ) )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 < 𝐵 ) ∧ 𝑞 ∈ ℚ ) → ( ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) → 𝑞 ∈ ( 𝐴 (,) 𝐵 ) ) )
20 19 reximdva ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( ∃ 𝑞 ∈ ℚ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) → ∃ 𝑞 ∈ ℚ 𝑞 ∈ ( 𝐴 (,) 𝐵 ) ) )
21 10 20 mpd ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ∃ 𝑞 ∈ ℚ 𝑞 ∈ ( 𝐴 (,) 𝐵 ) )
22 inn0 ⊢ ( ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ ↔ ∃ 𝑞 ∈ ℚ 𝑞 ∈ ( 𝐴 (,) 𝐵 ) )
23 21 22 sylibr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ )
24 5 23 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ )
25 24 neneqd ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
26 25 adantlr ⊢ ( ( ( 𝜑 ∧ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
27 3 26 condan ⊢ ( ( 𝜑 ∧ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) → 𝐵 ≤ 𝐴 )
28 ioo0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
29 1 2 28 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
30 29 biimpar ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
31 ineq2 ⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ( ℚ ∩ ∅ ) )
32 in0 ⊢ ( ℚ ∩ ∅ ) = ∅
33 31 32 eqtrdi ⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
34 30 33 syl ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
35 27 34 impbida ⊢ ( 𝜑 → ( ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )