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
|- ( 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 ) )