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 \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
	dya2icoseg.1	$⊢ N = ⌊1 - \log_{2} D⌋$
Assertion	dya2icoseg	$⊢ (X \in ℝ \land D \in ℝ^{+}) \to \exists b \in ran I (X \in b \land b \subseteq (X - D, X + D))$

Proof

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

Metamath Proof Explorer

Theorem dya2icoseg

Proof