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

Metamath Proof Explorer

Theorem qelioo

Description: The rational numbers are dense in RR* : any two extended real numbers have a rational between them. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses qelioo.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
qelioo.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
qelioo.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion qelioo ( 𝜑 → ∃ 𝑥 ∈ ℚ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 qelioo.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 qelioo.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 qelioo.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 qbtwnxr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
5 1 2 3 4 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
6 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝐴 ∈ ℝ* )
7 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝐵 ∈ ℝ* )
8 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
9 8 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝑥 ∈ ℝ )
10 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝐴 < 𝑥 )
11 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝑥 < 𝐵 )
12 6 7 9 10 11 eliood ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
13 12 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℚ ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
14 13 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → ∃ 𝑥 ∈ ℚ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
15 5 14 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℚ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )