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	|- ( ph -> A e. RR* )
	qelioo.2	|- ( ph -> B e. RR* )
	qelioo.3	|- ( ph -> A < B )
Assertion	qelioo	|- ( ph -> E. x e. QQ x e. ( A (,) B ) )

Proof

Step	Hyp	Ref	Expression
1		qelioo.1	|- ( ph -> A e. RR* )
2		qelioo.2	|- ( ph -> B e. RR* )
3		qelioo.3	|- ( ph -> A < B )
4		qbtwnxr	|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )
5	1 2 3 4	syl3anc	|- ( ph -> E. x e. QQ ( A < x /\ x < B ) )
6	1	ad2antrr	|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> A e. RR* )
7	2	ad2antrr	|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> B e. RR* )
8		qre	|- ( x e. QQ -> x e. RR )
9	8	ad2antlr	|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x e. RR )
10		simprl	|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> A < x )
11		simprr	|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x < B )
12	6 7 9 10 11	eliood	|- ( ( ( ph /\ x e. QQ ) /\ ( A < x /\ x < B ) ) -> x e. ( A (,) B ) )
13	12	ex	|- ( ( ph /\ x e. QQ ) -> ( ( A < x /\ x < B ) -> x e. ( A (,) B ) ) )
14	13	reximdva	|- ( ph -> ( E. x e. QQ ( A < x /\ x < B ) -> E. x e. QQ x e. ( A (,) B ) ) )
15	5 14	mpd	|- ( ph -> E. x e. QQ x e. ( A (,) B ) )