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	$⊢ φ \to A \in ℝ^{*}$
		qelioo.2	$⊢ φ \to B \in ℝ^{*}$
		qelioo.3	$⊢ φ \to A < B$
	Assertion	qelioo	$⊢ φ \to \exists x \in ℚ x \in (A, B)$

Proof

Step	Hyp	Ref	Expression
1		qelioo.1	$⊢ φ \to A \in ℝ^{*}$
2		qelioo.2	$⊢ φ \to B \in ℝ^{*}$
3		qelioo.3	$⊢ φ \to A < B$
4		qbtwnxr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℚ (A < x \land x < B)$
5	1 2 3 4	syl3anc	$⊢ φ \to \exists x \in ℚ (A < x \land x < B)$
6	1	ad2antrr	$⊢ ((φ \land x \in ℚ) \land (A < x \land x < B)) \to A \in ℝ^{*}$
7	2	ad2antrr	$⊢ ((φ \land x \in ℚ) \land (A < x \land x < B)) \to B \in ℝ^{*}$
8		qre	$⊢ x \in ℚ \to x \in ℝ$
9	8	ad2antlr	$⊢ ((φ \land x \in ℚ) \land (A < x \land x < B)) \to x \in ℝ$
10		simprl	$⊢ ((φ \land x \in ℚ) \land (A < x \land x < B)) \to A < x$
11		simprr	$⊢ ((φ \land x \in ℚ) \land (A < x \land x < B)) \to x < B$
12	6 7 9 10 11	eliood	$⊢ ((φ \land x \in ℚ) \land (A < x \land x < B)) \to x \in (A, B)$
13	12	ex	$⊢ (φ \land x \in ℚ) \to ((A < x \land x < B) \to x \in (A, B))$
14	13	reximdva	$⊢ φ \to (\exists x \in ℚ (A < x \land x < B) \to \exists x \in ℚ x \in (A, B))$
15	5 14	mpd	$⊢ φ \to \exists x \in ℚ x \in (A, B)$