Metamath Proof Explorer

Theorem dya2icoseg

Description: For any point and any closed-below, open-above interval of RR centered on that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 19-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 
|- J = ( topGen ` ran (,) )
dya2ioc.1 
|- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
dya2icoseg.1 
|- N = ( |_ ` ( 1 - ( 2 logb D ) ) )
Assertion dya2icoseg 
|- ( ( X e. RR /\ D e. RR+ ) -> E. b e. ran I ( X e. b /\ b C_ ( ( X - D ) (,) ( X + D ) ) ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 dya2ioc.1 
 |-  I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
3 dya2icoseg.1 
 |-  N = ( |_ ` ( 1 - ( 2 logb D ) ) )
4 ovex 
 |-  ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. _V
5 2 4 fnmpoi 
 |-  I Fn ( ZZ X. ZZ )
6 5 a1i 
 |-  ( ( X e. RR /\ D e. RR+ ) -> I Fn ( ZZ X. ZZ ) )
7 simpl 
 |-  ( ( X e. RR /\ D e. RR+ ) -> X e. RR )
8 2rp 
 |-  2 e. RR+
9 1red 
 |-  ( D e. RR+ -> 1 e. RR )
10 2z 
 |-  2 e. ZZ
11 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
12 10 11 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
13 relogbzcl 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ D e. RR+ ) -> ( 2 logb D ) e. RR )
14 12 13 mpan 
 |-  ( D e. RR+ -> ( 2 logb D ) e. RR )
15 9 14 resubcld 
 |-  ( D e. RR+ -> ( 1 - ( 2 logb D ) ) e. RR )
16 15 flcld 
 |-  ( D e. RR+ -> ( |_ ` ( 1 - ( 2 logb D ) ) ) e. ZZ )
17 3 16 eqeltrid 
 |-  ( D e. RR+ -> N e. ZZ )
18 rpexpcl 
 |-  ( ( 2 e. RR+ /\ N e. ZZ ) -> ( 2 ^ N ) e. RR+ )
19 18 rpred 
 |-  ( ( 2 e. RR+ /\ N e. ZZ ) -> ( 2 ^ N ) e. RR )
20 8 17 19 sylancr 
 |-  ( D e. RR+ -> ( 2 ^ N ) e. RR )
21 20 adantl 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 2 ^ N ) e. RR )
22 7 21 remulcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X x. ( 2 ^ N ) ) e. RR )
23 22 flcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( |_ ` ( X x. ( 2 ^ N ) ) ) e. ZZ )
24 17 adantl 
 |-  ( ( X e. RR /\ D e. RR+ ) -> N e. ZZ )
25 fnovrn 
 |-  ( ( I Fn ( ZZ X. ZZ ) /\ ( |_ ` ( X x. ( 2 ^ N ) ) ) e. ZZ /\ N e. ZZ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) e. ran I )
26 6 23 24 25 syl3anc 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) e. ran I )
27 23 zred 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( |_ ` ( X x. ( 2 ^ N ) ) ) e. RR )
28 8 24 18 sylancr 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 2 ^ N ) e. RR+ )
29 fllelt 
 |-  ( ( X x. ( 2 ^ N ) ) e. RR -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) <_ ( X x. ( 2 ^ N ) ) /\ ( X x. ( 2 ^ N ) ) < ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) ) )
30 22 29 syl 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) <_ ( X x. ( 2 ^ N ) ) /\ ( X x. ( 2 ^ N ) ) < ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) ) )
31 30 simpld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( |_ ` ( X x. ( 2 ^ N ) ) ) <_ ( X x. ( 2 ^ N ) ) )
32 27 22 28 31 lediv1dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) <_ ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) )
33 7 recnd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> X e. CC )
34 21 recnd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 2 ^ N ) e. CC )
35 2cnd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> 2 e. CC )
36 2ne0 
 |-  2 =/= 0
37 36 a1i 
 |-  ( ( X e. RR /\ D e. RR+ ) -> 2 =/= 0 )
38 35 37 24 expne0d 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 2 ^ N ) =/= 0 )
39 33 34 38 divcan4d 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) = X )
40 32 39 breqtrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) <_ X )
41 1red 
 |-  ( ( X e. RR /\ D e. RR+ ) -> 1 e. RR )
42 27 41 readdcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) e. RR )
43 30 simprd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X x. ( 2 ^ N ) ) < ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) )
44 22 42 28 43 ltdiv1dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) < ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) )
45 39 44 eqbrtrrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> X < ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) )
46 27 21 38 redivcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) e. RR )
47 42 21 38 redivcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) e. RR )
48 47 rexrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) e. RR* )
49 elico2 
 |-  ( ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) e. RR /\ ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) e. RR* ) -> ( X e. ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) <-> ( X e. RR /\ ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) <_ X /\ X < ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) ) )
50 46 48 49 syl2anc 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X e. ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) <-> ( X e. RR /\ ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) <_ X /\ X < ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) ) )
51 7 40 45 50 mpbir3and 
 |-  ( ( X e. RR /\ D e. RR+ ) -> X e. ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) )
52 1 2 dya2iocival 
 |-  ( ( N e. ZZ /\ ( |_ ` ( X x. ( 2 ^ N ) ) ) e. ZZ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) = ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) )
53 24 23 52 syl2anc 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) = ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) )
54 51 53 eleqtrrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> X e. ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) )
55 simpr 
 |-  ( ( X e. RR /\ D e. RR+ ) -> D e. RR+ )
56 55 rpred 
 |-  ( ( X e. RR /\ D e. RR+ ) -> D e. RR )
57 7 56 resubcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X - D ) e. RR )
58 57 rexrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X - D ) e. RR* )
59 7 56 readdcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X + D ) e. RR )
60 59 rexrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X + D ) e. RR* )
61 21 38 rereccld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 1 / ( 2 ^ N ) ) e. RR )
62 7 61 resubcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X - ( 1 / ( 2 ^ N ) ) ) e. RR )
63 3 oveq2i 
 |-  ( 2 ^ N ) = ( 2 ^ ( |_ ` ( 1 - ( 2 logb D ) ) ) )
64 63 oveq2i 
 |-  ( 1 / ( 2 ^ N ) ) = ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb D ) ) ) ) )
65 dya2ub 
 |-  ( D e. RR+ -> ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb D ) ) ) ) ) < D )
66 65 adantl 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb D ) ) ) ) ) < D )
67 64 66 eqbrtrid 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( 1 / ( 2 ^ N ) ) < D )
68 61 56 7 67 ltsub2dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X - D ) < ( X - ( 1 / ( 2 ^ N ) ) ) )
69 33 34 mulcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X x. ( 2 ^ N ) ) e. CC )
70 1cnd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> 1 e. CC )
71 69 70 34 38 divsubdird 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) - 1 ) / ( 2 ^ N ) ) = ( ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) - ( 1 / ( 2 ^ N ) ) ) )
72 39 oveq1d 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) - ( 1 / ( 2 ^ N ) ) ) = ( X - ( 1 / ( 2 ^ N ) ) ) )
73 71 72 eqtrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) - 1 ) / ( 2 ^ N ) ) = ( X - ( 1 / ( 2 ^ N ) ) ) )
74 22 41 resubcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) - 1 ) e. RR )
75 22 42 41 43 ltsub1dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) - 1 ) < ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) - 1 ) )
76 27 recnd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( |_ ` ( X x. ( 2 ^ N ) ) ) e. CC )
77 76 70 pncand 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) - 1 ) = ( |_ ` ( X x. ( 2 ^ N ) ) ) )
78 75 77 breqtrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) - 1 ) < ( |_ ` ( X x. ( 2 ^ N ) ) ) )
79 74 27 78 ltled 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) - 1 ) <_ ( |_ ` ( X x. ( 2 ^ N ) ) ) )
80 74 27 28 79 lediv1dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) - 1 ) / ( 2 ^ N ) ) <_ ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
81 73 80 eqbrtrrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X - ( 1 / ( 2 ^ N ) ) ) <_ ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
82 57 62 46 68 81 ltletrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X - D ) < ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
83 7 61 readdcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X + ( 1 / ( 2 ^ N ) ) ) e. RR )
84 22 41 readdcld 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( X x. ( 2 ^ N ) ) + 1 ) e. RR )
85 27 22 41 31 leadd1dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) <_ ( ( X x. ( 2 ^ N ) ) + 1 ) )
86 42 84 28 85 lediv1dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) <_ ( ( ( X x. ( 2 ^ N ) ) + 1 ) / ( 2 ^ N ) ) )
87 69 70 34 38 divdird 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) + 1 ) / ( 2 ^ N ) ) = ( ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) + ( 1 / ( 2 ^ N ) ) ) )
88 39 oveq1d 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) / ( 2 ^ N ) ) + ( 1 / ( 2 ^ N ) ) ) = ( X + ( 1 / ( 2 ^ N ) ) ) )
89 87 88 eqtrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( X x. ( 2 ^ N ) ) + 1 ) / ( 2 ^ N ) ) = ( X + ( 1 / ( 2 ^ N ) ) ) )
90 86 89 breqtrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) <_ ( X + ( 1 / ( 2 ^ N ) ) ) )
91 61 56 7 67 ltadd2dd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( X + ( 1 / ( 2 ^ N ) ) ) < ( X + D ) )
92 47 83 59 90 91 lelttrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) < ( X + D ) )
93 47 59 92 ltled 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) <_ ( X + D ) )
94 icossioo 
 |-  ( ( ( ( X - D ) e. RR* /\ ( X + D ) e. RR* ) /\ ( ( X - D ) < ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) /\ ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) <_ ( X + D ) ) ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) C_ ( ( X - D ) (,) ( X + D ) ) )
95 58 60 82 93 94 syl22anc 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) / ( 2 ^ N ) ) [,) ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) + 1 ) / ( 2 ^ N ) ) ) C_ ( ( X - D ) (,) ( X + D ) ) )
96 53 95 eqsstrd 
 |-  ( ( X e. RR /\ D e. RR+ ) -> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) C_ ( ( X - D ) (,) ( X + D ) ) )
97 eleq2 
 |-  ( b = ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) -> ( X e. b <-> X e. ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) ) )
98 sseq1 
 |-  ( b = ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) -> ( b C_ ( ( X - D ) (,) ( X + D ) ) <-> ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) C_ ( ( X - D ) (,) ( X + D ) ) ) )
99 97 98 anbi12d 
 |-  ( b = ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) -> ( ( X e. b /\ b C_ ( ( X - D ) (,) ( X + D ) ) ) <-> ( X e. ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) /\ ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) C_ ( ( X - D ) (,) ( X + D ) ) ) ) )
100 99 rspcev 
 |-  ( ( ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) e. ran I /\ ( X e. ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) /\ ( ( |_ ` ( X x. ( 2 ^ N ) ) ) I N ) C_ ( ( X - D ) (,) ( X + D ) ) ) ) -> E. b e. ran I ( X e. b /\ b C_ ( ( X - D ) (,) ( X + D ) ) ) )
101 26 54 96 100 syl12anc 
 |-  ( ( X e. RR /\ D e. RR+ ) -> E. b e. ran I ( X e. b /\ b C_ ( ( X - D ) (,) ( X + D ) ) ) )