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