This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qinioo

Description: The rational numbers are dense in RR . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses qinioo.a 
|- ( ph -> A e. RR* )
qinioo.b 
|- ( ph -> B e. RR* )
Assertion qinioo 
|- ( ph -> ( ( QQ i^i ( A (,) B ) ) = (/) <-> B <_ A ) )

Proof

Step Hyp Ref Expression
1 qinioo.a 
 |-  ( ph -> A e. RR* )
2 qinioo.b 
 |-  ( ph -> B e. RR* )
3 simplr 
 |-  ( ( ( ph /\ ( QQ i^i ( A (,) B ) ) = (/) ) /\ -. B <_ A ) -> ( QQ i^i ( A (,) B ) ) = (/) )
4 1 2 xrltnled 
 |-  ( ph -> ( A < B <-> -. B <_ A ) )
5 4 biimpar 
 |-  ( ( ph /\ -. B <_ A ) -> A < B )
6 1 adantr 
 |-  ( ( ph /\ A < B ) -> A e. RR* )
7 2 adantr 
 |-  ( ( ph /\ A < B ) -> B e. RR* )
8 simpr 
 |-  ( ( ph /\ A < B ) -> A < B )
9 qbtwnxr 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. q e. QQ ( A < q /\ q < B ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ph /\ A < B ) -> E. q e. QQ ( A < q /\ q < B ) )
11 1 ad2antrr 
 |-  ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> A e. RR* )
12 2 ad2antrr 
 |-  ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> B e. RR* )
13 qre 
 |-  ( q e. QQ -> q e. RR )
14 13 ad2antlr 
 |-  ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> q e. RR )
15 simprl 
 |-  ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> A < q )
16 simprr 
 |-  ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> q < B )
17 11 12 14 15 16 eliood 
 |-  ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> q e. ( A (,) B ) )
18 17 ex 
 |-  ( ( ph /\ q e. QQ ) -> ( ( A < q /\ q < B ) -> q e. ( A (,) B ) ) )
19 18 adantlr 
 |-  ( ( ( ph /\ A < B ) /\ q e. QQ ) -> ( ( A < q /\ q < B ) -> q e. ( A (,) B ) ) )
20 19 reximdva 
 |-  ( ( ph /\ A < B ) -> ( E. q e. QQ ( A < q /\ q < B ) -> E. q e. QQ q e. ( A (,) B ) ) )
21 10 20 mpd 
 |-  ( ( ph /\ A < B ) -> E. q e. QQ q e. ( A (,) B ) )
22 inn0 
 |-  ( ( QQ i^i ( A (,) B ) ) =/= (/) <-> E. q e. QQ q e. ( A (,) B ) )
23 21 22 sylibr 
 |-  ( ( ph /\ A < B ) -> ( QQ i^i ( A (,) B ) ) =/= (/) )
24 5 23 syldan 
 |-  ( ( ph /\ -. B <_ A ) -> ( QQ i^i ( A (,) B ) ) =/= (/) )
25 24 neneqd 
 |-  ( ( ph /\ -. B <_ A ) -> -. ( QQ i^i ( A (,) B ) ) = (/) )
26 25 adantlr 
 |-  ( ( ( ph /\ ( QQ i^i ( A (,) B ) ) = (/) ) /\ -. B <_ A ) -> -. ( QQ i^i ( A (,) B ) ) = (/) )
27 3 26 condan 
 |-  ( ( ph /\ ( QQ i^i ( A (,) B ) ) = (/) ) -> B <_ A )
28 ioo0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
29 1 2 28 syl2anc 
 |-  ( ph -> ( ( A (,) B ) = (/) <-> B <_ A ) )
30 29 biimpar 
 |-  ( ( ph /\ B <_ A ) -> ( A (,) B ) = (/) )
31 ineq2 
 |-  ( ( A (,) B ) = (/) -> ( QQ i^i ( A (,) B ) ) = ( QQ i^i (/) ) )
32 in0 
 |-  ( QQ i^i (/) ) = (/)
33 31 32 eqtrdi 
 |-  ( ( A (,) B ) = (/) -> ( QQ i^i ( A (,) B ) ) = (/) )
34 30 33 syl 
 |-  ( ( ph /\ B <_ A ) -> ( QQ i^i ( A (,) B ) ) = (/) )
35 27 34 impbida 
 |-  ( ph -> ( ( QQ i^i ( A (,) B ) ) = (/) <-> B <_ A ) )