Metamath Proof Explorer

Theorem qbtwnre

Description: The rational numbers are dense in RR : any two real numbers have a rational between them. Exercise 6 of Apostol p. 28. (Contributed by NM, 18-Nov-2004) (Proof shortened by Mario Carneiro, 13-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 posdif 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )
2 resubcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
3 nnrecl 
 |-  ( ( ( B - A ) e. RR /\ 0 < ( B - A ) ) -> E. y e. NN ( 1 / y ) < ( B - A ) )
4 2 3 sylan 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ 0 < ( B - A ) ) -> E. y e. NN ( 1 / y ) < ( B - A ) )
5 4 ex 
 |-  ( ( B e. RR /\ A e. RR ) -> ( 0 < ( B - A ) -> E. y e. NN ( 1 / y ) < ( B - A ) ) )
6 5 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( B - A ) -> E. y e. NN ( 1 / y ) < ( B - A ) ) )
7 1 6 sylbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> E. y e. NN ( 1 / y ) < ( B - A ) ) )
8 nnre 
 |-  ( y e. NN -> y e. RR )
9 8 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> y e. RR )
10 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> B e. RR )
11 9 10 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> ( y x. B ) e. RR )
12 peano2rem 
 |-  ( ( y x. B ) e. RR -> ( ( y x. B ) - 1 ) e. RR )
13 11 12 syl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> ( ( y x. B ) - 1 ) e. RR )
14 zbtwnre 
 |-  ( ( ( y x. B ) - 1 ) e. RR -> E! z e. ZZ ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) )
15 reurex 
 |-  ( E! z e. ZZ ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) -> E. z e. ZZ ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) )
16 13 14 15 3syl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> E. z e. ZZ ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) )
17 znq 
 |-  ( ( z e. ZZ /\ y e. NN ) -> ( z / y ) e. QQ )
18 17 ancoms 
 |-  ( ( y e. NN /\ z e. ZZ ) -> ( z / y ) e. QQ )
19 18 adantl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( z / y ) e. QQ )
20 an32 
 |-  ( ( ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) /\ ( 1 / y ) < ( B - A ) ) <-> ( ( ( ( y x. B ) - 1 ) <_ z /\ ( 1 / y ) < ( B - A ) ) /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) )
21 8 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> y e. RR )
22 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> A e. RR )
23 21 22 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( y x. A ) e. RR )
24 13 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( y x. B ) - 1 ) e. RR )
25 zre 
 |-  ( z e. ZZ -> z e. RR )
26 25 ad2antll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> z e. RR )
27 ltletr 
 |-  ( ( ( y x. A ) e. RR /\ ( ( y x. B ) - 1 ) e. RR /\ z e. RR ) -> ( ( ( y x. A ) < ( ( y x. B ) - 1 ) /\ ( ( y x. B ) - 1 ) <_ z ) -> ( y x. A ) < z ) )
28 23 24 26 27 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( y x. A ) < ( ( y x. B ) - 1 ) /\ ( ( y x. B ) - 1 ) <_ z ) -> ( y x. A ) < z ) )
29 21 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> y e. CC )
30 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> B e. RR )
31 30 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> B e. CC )
32 22 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> A e. CC )
33 29 31 32 subdid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( y x. ( B - A ) ) = ( ( y x. B ) - ( y x. A ) ) )
34 33 breq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( 1 < ( y x. ( B - A ) ) <-> 1 < ( ( y x. B ) - ( y x. A ) ) ) )
35 1red 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> 1 e. RR )
36 30 22 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( B - A ) e. RR )
37 nngt0 
 |-  ( y e. NN -> 0 < y )
38 37 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> 0 < y )
39 ltdivmul 
 |-  ( ( 1 e. RR /\ ( B - A ) e. RR /\ ( y e. RR /\ 0 < y ) ) -> ( ( 1 / y ) < ( B - A ) <-> 1 < ( y x. ( B - A ) ) ) )
40 35 36 21 38 39 syl112anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( 1 / y ) < ( B - A ) <-> 1 < ( y x. ( B - A ) ) ) )
41 11 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( y x. B ) e. RR )
42 ltsub13 
 |-  ( ( ( y x. A ) e. RR /\ ( y x. B ) e. RR /\ 1 e. RR ) -> ( ( y x. A ) < ( ( y x. B ) - 1 ) <-> 1 < ( ( y x. B ) - ( y x. A ) ) ) )
43 23 41 35 42 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( y x. A ) < ( ( y x. B ) - 1 ) <-> 1 < ( ( y x. B ) - ( y x. A ) ) ) )
44 34 40 43 3bitr4rd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( y x. A ) < ( ( y x. B ) - 1 ) <-> ( 1 / y ) < ( B - A ) ) )
45 44 anbi1d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( y x. A ) < ( ( y x. B ) - 1 ) /\ ( ( y x. B ) - 1 ) <_ z ) <-> ( ( 1 / y ) < ( B - A ) /\ ( ( y x. B ) - 1 ) <_ z ) ) )
46 45 biancomd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( y x. A ) < ( ( y x. B ) - 1 ) /\ ( ( y x. B ) - 1 ) <_ z ) <-> ( ( ( y x. B ) - 1 ) <_ z /\ ( 1 / y ) < ( B - A ) ) ) )
47 ltmuldiv2 
 |-  ( ( A e. RR /\ z e. RR /\ ( y e. RR /\ 0 < y ) ) -> ( ( y x. A ) < z <-> A < ( z / y ) ) )
48 22 26 21 38 47 syl112anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( y x. A ) < z <-> A < ( z / y ) ) )
49 28 46 48 3imtr3d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( ( y x. B ) - 1 ) <_ z /\ ( 1 / y ) < ( B - A ) ) -> A < ( z / y ) ) )
50 41 recnd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( y x. B ) e. CC )
51 ax-1cn 
 |-  1 e. CC
52 npcan 
 |-  ( ( ( y x. B ) e. CC /\ 1 e. CC ) -> ( ( ( y x. B ) - 1 ) + 1 ) = ( y x. B ) )
53 50 51 52 sylancl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( y x. B ) - 1 ) + 1 ) = ( y x. B ) )
54 53 breq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( z < ( ( ( y x. B ) - 1 ) + 1 ) <-> z < ( y x. B ) ) )
55 ltdivmul 
 |-  ( ( z e. RR /\ B e. RR /\ ( y e. RR /\ 0 < y ) ) -> ( ( z / y ) < B <-> z < ( y x. B ) ) )
56 26 30 21 38 55 syl112anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( z / y ) < B <-> z < ( y x. B ) ) )
57 54 56 bitr4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( z < ( ( ( y x. B ) - 1 ) + 1 ) <-> ( z / y ) < B ) )
58 57 biimpd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( z < ( ( ( y x. B ) - 1 ) + 1 ) -> ( z / y ) < B ) )
59 49 58 anim12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( ( ( y x. B ) - 1 ) <_ z /\ ( 1 / y ) < ( B - A ) ) /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) -> ( A < ( z / y ) /\ ( z / y ) < B ) ) )
60 20 59 syl5bi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) /\ ( 1 / y ) < ( B - A ) ) -> ( A < ( z / y ) /\ ( z / y ) < B ) ) )
61 breq2 
 |-  ( x = ( z / y ) -> ( A < x <-> A < ( z / y ) ) )
62 breq1 
 |-  ( x = ( z / y ) -> ( x < B <-> ( z / y ) < B ) )
63 61 62 anbi12d 
 |-  ( x = ( z / y ) -> ( ( A < x /\ x < B ) <-> ( A < ( z / y ) /\ ( z / y ) < B ) ) )
64 63 rspcev 
 |-  ( ( ( z / y ) e. QQ /\ ( A < ( z / y ) /\ ( z / y ) < B ) ) -> E. x e. QQ ( A < x /\ x < B ) )
65 19 60 64 syl6an 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) /\ ( 1 / y ) < ( B - A ) ) -> E. x e. QQ ( A < x /\ x < B ) ) )
66 65 expd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) -> ( ( 1 / y ) < ( B - A ) -> E. x e. QQ ( A < x /\ x < B ) ) ) )
67 66 expr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> ( z e. ZZ -> ( ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) -> ( ( 1 / y ) < ( B - A ) -> E. x e. QQ ( A < x /\ x < B ) ) ) ) )
68 67 rexlimdv 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> ( E. z e. ZZ ( ( ( y x. B ) - 1 ) <_ z /\ z < ( ( ( y x. B ) - 1 ) + 1 ) ) -> ( ( 1 / y ) < ( B - A ) -> E. x e. QQ ( A < x /\ x < B ) ) ) )
69 16 68 mpd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ y e. NN ) -> ( ( 1 / y ) < ( B - A ) -> E. x e. QQ ( A < x /\ x < B ) ) )
70 69 rexlimdva 
 |-  ( ( A e. RR /\ B e. RR ) -> ( E. y e. NN ( 1 / y ) < ( B - A ) -> E. x e. QQ ( A < x /\ x < B ) ) )
71 7 70 syld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> E. x e. QQ ( A < x /\ x < B ) ) )
72 71 3impia 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )