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