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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2icoseg.1 ⊢ 𝑁 = ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) )
Assertion dya2icoseg ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 dya2icoseg.1 ⊢ 𝑁 = ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) )
4 ovex ⊢ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V
5 2 4 fnmpoi ⊢ 𝐼 Fn ( ℤ × ℤ )
6 5 a1i ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐼 Fn ( ℤ × ℤ ) )
7 simpl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝑋 ∈ ℝ )
8 2rp ⊢ 2 ∈ ℝ+
9 1red ⊢ ( 𝐷 ∈ ℝ+ → 1 ∈ ℝ )
10 2z ⊢ 2 ∈ ℤ
11 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
12 10 11 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
13 relogbzcl ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐷 ∈ ℝ+ ) → ( 2 logb 𝐷 ) ∈ ℝ )
14 12 13 mpan ⊢ ( 𝐷 ∈ ℝ+ → ( 2 logb 𝐷 ) ∈ ℝ )
15 9 14 resubcld ⊢ ( 𝐷 ∈ ℝ+ → ( 1 − ( 2 logb 𝐷 ) ) ∈ ℝ )
16 15 flcld ⊢ ( 𝐷 ∈ ℝ+ → ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) ) ∈ ℤ )
17 3 16 eqeltrid ⊢ ( 𝐷 ∈ ℝ+ → 𝑁 ∈ ℤ )
18 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
19 18 rpred ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
20 8 17 19 sylancr ⊢ ( 𝐷 ∈ ℝ+ → ( 2 ↑ 𝑁 ) ∈ ℝ )
21 20 adantl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
22 7 21 remulcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 · ( 2 ↑ 𝑁 ) ) ∈ ℝ )
23 22 flcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ∈ ℤ )
24 17 adantl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝑁 ∈ ℤ )
25 fnovrn ⊢ ( ( 𝐼 Fn ( ℤ × ℤ ) ∧ ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ∈ ran 𝐼 )
26 6 23 24 25 syl3anc ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ∈ ran 𝐼 )
27 23 zred ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
28 8 24 18 sylancr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
29 fllelt ⊢ ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ≤ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ∧ ( 𝑋 · ( 2 ↑ 𝑁 ) ) < ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) ) )
30 22 29 syl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ≤ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ∧ ( 𝑋 · ( 2 ↑ 𝑁 ) ) < ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) ) )
31 30 simpld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ≤ ( 𝑋 · ( 2 ↑ 𝑁 ) ) )
32 27 22 28 31 lediv1dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) )
33 7 recnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝑋 ∈ ℂ )
34 21 recnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
35 2cnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 2 ∈ ℂ )
36 2ne0 ⊢ 2 ≠ 0
37 36 a1i ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 2 ≠ 0 )
38 35 37 24 expne0d ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 2 ↑ 𝑁 ) ≠ 0 )
39 33 34 38 divcan4d ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) = 𝑋 )
40 32 39 breqtrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ≤ 𝑋 )
41 1red ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 1 ∈ ℝ )
42 27 41 readdcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) ∈ ℝ )
43 30 simprd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 · ( 2 ↑ 𝑁 ) ) < ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) )
44 22 42 28 43 ltdiv1dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) < ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) )
45 39 44 eqbrtrrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝑋 < ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) )
46 27 21 38 redivcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
47 42 21 38 redivcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
48 47 rexrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ* )
49 elico2 ⊢ ( ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ* ) → ( 𝑋 ∈ ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) ↔ ( 𝑋 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ≤ 𝑋 ∧ 𝑋 < ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) ) )
50 46 48 49 syl2anc ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 ∈ ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) ↔ ( 𝑋 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ≤ 𝑋 ∧ 𝑋 < ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) ) )
51 7 40 45 50 mpbir3and ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝑋 ∈ ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
52 1 2 dya2iocival ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) = ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
53 24 23 52 syl2anc ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) = ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
54 51 53 eleqtrrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝑋 ∈ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) )
55 simpr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℝ+ )
56 55 rpred ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℝ )
57 7 56 resubcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 − 𝐷 ) ∈ ℝ )
58 57 rexrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 − 𝐷 ) ∈ ℝ* )
59 7 56 readdcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 + 𝐷 ) ∈ ℝ )
60 59 rexrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 + 𝐷 ) ∈ ℝ* )
61 21 38 rereccld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 1 / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
62 7 61 resubcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 − ( 1 / ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
63 3 oveq2i ⊢ ( 2 ↑ 𝑁 ) = ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) ) )
64 63 oveq2i ⊢ ( 1 / ( 2 ↑ 𝑁 ) ) = ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) ) ) )
65 dya2ub ⊢ ( 𝐷 ∈ ℝ+ → ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) ) ) ) < 𝐷 )
66 65 adantl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝐷 ) ) ) ) ) < 𝐷 )
67 64 66 eqbrtrid ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 1 / ( 2 ↑ 𝑁 ) ) < 𝐷 )
68 61 56 7 67 ltsub2dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 − 𝐷 ) < ( 𝑋 − ( 1 / ( 2 ↑ 𝑁 ) ) ) )
69 33 34 mulcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 · ( 2 ↑ 𝑁 ) ) ∈ ℂ )
70 1cnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 1 ∈ ℂ )
71 69 70 34 38 divsubdird ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) / ( 2 ↑ 𝑁 ) ) = ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) − ( 1 / ( 2 ↑ 𝑁 ) ) ) )
72 39 oveq1d ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) − ( 1 / ( 2 ↑ 𝑁 ) ) ) = ( 𝑋 − ( 1 / ( 2 ↑ 𝑁 ) ) ) )
73 71 72 eqtrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) / ( 2 ↑ 𝑁 ) ) = ( 𝑋 − ( 1 / ( 2 ↑ 𝑁 ) ) ) )
74 22 41 resubcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) ∈ ℝ )
75 22 42 41 43 ltsub1dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) < ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) − 1 ) )
76 27 recnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) ∈ ℂ )
77 76 70 pncand ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) − 1 ) = ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) )
78 75 77 breqtrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) < ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) )
79 74 27 78 ltled ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) ≤ ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) )
80 74 27 28 79 lediv1dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) − 1 ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
81 73 80 eqbrtrrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 − ( 1 / ( 2 ↑ 𝑁 ) ) ) ≤ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
82 57 62 46 68 81 ltletrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 − 𝐷 ) < ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
83 7 61 readdcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 + ( 1 / ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
84 22 41 readdcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℝ )
85 27 22 41 31 leadd1dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) ≤ ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) + 1 ) )
86 42 84 28 85 lediv1dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) )
87 69 70 34 38 divdird ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) = ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) + ( 1 / ( 2 ↑ 𝑁 ) ) ) )
88 39 oveq1d ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) + ( 1 / ( 2 ↑ 𝑁 ) ) ) = ( 𝑋 + ( 1 / ( 2 ↑ 𝑁 ) ) ) )
89 87 88 eqtrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 2 ↑ 𝑁 ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) = ( 𝑋 + ( 1 / ( 2 ↑ 𝑁 ) ) ) )
90 86 89 breqtrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ≤ ( 𝑋 + ( 1 / ( 2 ↑ 𝑁 ) ) ) )
91 61 56 7 67 ltadd2dd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝑋 + ( 1 / ( 2 ↑ 𝑁 ) ) ) < ( 𝑋 + 𝐷 ) )
92 47 83 59 90 91 lelttrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) < ( 𝑋 + 𝐷 ) )
93 47 59 92 ltled ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ≤ ( 𝑋 + 𝐷 ) )
94 icossioo ⊢ ( ( ( ( 𝑋 − 𝐷 ) ∈ ℝ* ∧ ( 𝑋 + 𝐷 ) ∈ ℝ* ) ∧ ( ( 𝑋 − 𝐷 ) < ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∧ ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ≤ ( 𝑋 + 𝐷 ) ) ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) )
95 58 60 82 93 94 syl22anc ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) [,) ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) + 1 ) / ( 2 ↑ 𝑁 ) ) ) ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) )
96 53 95 eqsstrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) )
97 eleq2 ⊢ ( 𝑏 = ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ) )
98 sseq1 ⊢ ( 𝑏 = ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) → ( 𝑏 ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ↔ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) )
99 97 98 anbi12d ⊢ ( 𝑏 = ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) → ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) ↔ ( 𝑋 ∈ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ∧ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) ) )
100 99 rspcev ⊢ ( ( ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ∈ ran 𝐼 ∧ ( 𝑋 ∈ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ∧ ( ( ⌊ ‘ ( 𝑋 · ( 2 ↑ 𝑁 ) ) ) 𝐼 𝑁 ) ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) )
101 26 54 96 100 syl12anc ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝐷 ) (,) ( 𝑋 + 𝐷 ) ) ) )