Metamath Proof Explorer

Theorem qbtwnxr

Description: The rational numbers are dense in RR* : any two extended real numbers have a rational between them. (Contributed by NM, 6-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion qbtwnxr 
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
3 qbtwnre 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )
4 3 3expia 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
5 simpl 
 |-  ( ( A e. RR /\ B = +oo ) -> A e. RR )
6 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
7 6 adantr 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A + 1 ) e. RR )
8 ltp1 
 |-  ( A e. RR -> A < ( A + 1 ) )
9 8 adantr 
 |-  ( ( A e. RR /\ B = +oo ) -> A < ( A + 1 ) )
10 qbtwnre 
 |-  ( ( A e. RR /\ ( A + 1 ) e. RR /\ A < ( A + 1 ) ) -> E. x e. QQ ( A < x /\ x < ( A + 1 ) ) )
11 5 7 9 10 syl3anc 
 |-  ( ( A e. RR /\ B = +oo ) -> E. x e. QQ ( A < x /\ x < ( A + 1 ) ) )
12 qre 
 |-  ( x e. QQ -> x e. RR )
13 12 ltpnfd 
 |-  ( x e. QQ -> x < +oo )
14 13 adantl 
 |-  ( ( ( A e. RR /\ B = +oo ) /\ x e. QQ ) -> x < +oo )
15 simplr 
 |-  ( ( ( A e. RR /\ B = +oo ) /\ x e. QQ ) -> B = +oo )
16 14 15 breqtrrd 
 |-  ( ( ( A e. RR /\ B = +oo ) /\ x e. QQ ) -> x < B )
17 16 a1d 
 |-  ( ( ( A e. RR /\ B = +oo ) /\ x e. QQ ) -> ( x < ( A + 1 ) -> x < B ) )
18 17 anim2d 
 |-  ( ( ( A e. RR /\ B = +oo ) /\ x e. QQ ) -> ( ( A < x /\ x < ( A + 1 ) ) -> ( A < x /\ x < B ) ) )
19 18 reximdva 
 |-  ( ( A e. RR /\ B = +oo ) -> ( E. x e. QQ ( A < x /\ x < ( A + 1 ) ) -> E. x e. QQ ( A < x /\ x < B ) ) )
20 11 19 mpd 
 |-  ( ( A e. RR /\ B = +oo ) -> E. x e. QQ ( A < x /\ x < B ) )
21 20 a1d 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
22 rexr 
 |-  ( A e. RR -> A e. RR* )
23 breq2 
 |-  ( B = -oo -> ( A < B <-> A < -oo ) )
24 23 adantl 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( A < B <-> A < -oo ) )
25 nltmnf 
 |-  ( A e. RR* -> -. A < -oo )
26 25 adantr 
 |-  ( ( A e. RR* /\ B = -oo ) -> -. A < -oo )
27 26 pm2.21d 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( A < -oo -> E. x e. QQ ( A < x /\ x < B ) ) )
28 24 27 sylbid 
 |-  ( ( A e. RR* /\ B = -oo ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
29 22 28 sylan 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
30 4 21 29 3jaodan 
 |-  ( ( A e. RR /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
31 2 30 sylan2b 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
32 breq1 
 |-  ( A = +oo -> ( A < B <-> +oo < B ) )
33 32 adantr 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A < B <-> +oo < B ) )
34 pnfnlt 
 |-  ( B e. RR* -> -. +oo < B )
35 34 adantl 
 |-  ( ( A = +oo /\ B e. RR* ) -> -. +oo < B )
36 35 pm2.21d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( +oo < B -> E. x e. QQ ( A < x /\ x < B ) ) )
37 33 36 sylbid 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
38 peano2rem 
 |-  ( B e. RR -> ( B - 1 ) e. RR )
39 38 adantl 
 |-  ( ( A = -oo /\ B e. RR ) -> ( B - 1 ) e. RR )
40 simpr 
 |-  ( ( A = -oo /\ B e. RR ) -> B e. RR )
41 ltm1 
 |-  ( B e. RR -> ( B - 1 ) < B )
42 41 adantl 
 |-  ( ( A = -oo /\ B e. RR ) -> ( B - 1 ) < B )
43 qbtwnre 
 |-  ( ( ( B - 1 ) e. RR /\ B e. RR /\ ( B - 1 ) < B ) -> E. x e. QQ ( ( B - 1 ) < x /\ x < B ) )
44 39 40 42 43 syl3anc 
 |-  ( ( A = -oo /\ B e. RR ) -> E. x e. QQ ( ( B - 1 ) < x /\ x < B ) )
45 simpll 
 |-  ( ( ( A = -oo /\ B e. RR ) /\ x e. QQ ) -> A = -oo )
46 12 adantl 
 |-  ( ( ( A = -oo /\ B e. RR ) /\ x e. QQ ) -> x e. RR )
47 46 mnfltd 
 |-  ( ( ( A = -oo /\ B e. RR ) /\ x e. QQ ) -> -oo < x )
48 45 47 eqbrtrd 
 |-  ( ( ( A = -oo /\ B e. RR ) /\ x e. QQ ) -> A < x )
49 48 a1d 
 |-  ( ( ( A = -oo /\ B e. RR ) /\ x e. QQ ) -> ( ( B - 1 ) < x -> A < x ) )
50 49 anim1d 
 |-  ( ( ( A = -oo /\ B e. RR ) /\ x e. QQ ) -> ( ( ( B - 1 ) < x /\ x < B ) -> ( A < x /\ x < B ) ) )
51 50 reximdva 
 |-  ( ( A = -oo /\ B e. RR ) -> ( E. x e. QQ ( ( B - 1 ) < x /\ x < B ) -> E. x e. QQ ( A < x /\ x < B ) ) )
52 44 51 mpd 
 |-  ( ( A = -oo /\ B e. RR ) -> E. x e. QQ ( A < x /\ x < B ) )
53 52 a1d 
 |-  ( ( A = -oo /\ B e. RR ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
54 1re 
 |-  1 e. RR
55 mnflt 
 |-  ( 1 e. RR -> -oo < 1 )
56 54 55 ax-mp 
 |-  -oo < 1
57 breq1 
 |-  ( A = -oo -> ( A < 1 <-> -oo < 1 ) )
58 56 57 mpbiri 
 |-  ( A = -oo -> A < 1 )
59 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
60 54 59 ax-mp 
 |-  1 < +oo
61 breq2 
 |-  ( B = +oo -> ( 1 < B <-> 1 < +oo ) )
62 60 61 mpbiri 
 |-  ( B = +oo -> 1 < B )
63 1z 
 |-  1 e. ZZ
64 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
65 63 64 ax-mp 
 |-  1 e. QQ
66 breq2 
 |-  ( x = 1 -> ( A < x <-> A < 1 ) )
67 breq1 
 |-  ( x = 1 -> ( x < B <-> 1 < B ) )
68 66 67 anbi12d 
 |-  ( x = 1 -> ( ( A < x /\ x < B ) <-> ( A < 1 /\ 1 < B ) ) )
69 68 rspcev 
 |-  ( ( 1 e. QQ /\ ( A < 1 /\ 1 < B ) ) -> E. x e. QQ ( A < x /\ x < B ) )
70 65 69 mpan 
 |-  ( ( A < 1 /\ 1 < B ) -> E. x e. QQ ( A < x /\ x < B ) )
71 58 62 70 syl2an 
 |-  ( ( A = -oo /\ B = +oo ) -> E. x e. QQ ( A < x /\ x < B ) )
72 71 a1d 
 |-  ( ( A = -oo /\ B = +oo ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
73 3mix3 
 |-  ( A = -oo -> ( A e. RR \/ A = +oo \/ A = -oo ) )
74 73 1 sylibr 
 |-  ( A = -oo -> A e. RR* )
75 74 28 sylan 
 |-  ( ( A = -oo /\ B = -oo ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
76 53 72 75 3jaodan 
 |-  ( ( A = -oo /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
77 2 76 sylan2b 
 |-  ( ( A = -oo /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
78 31 37 77 3jaoian 
 |-  ( ( ( A e. RR \/ A = +oo \/ A = -oo ) /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
79 1 78 sylanb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
80 79 3impia 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )