dya2iocress

Description: Dyadic intervals are subsets of RR . (Contributed by Thierry Arnoux, 18-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}}))$
Assertion	dya2iocress	$⊢ (N \in ℤ \land X \in ℤ) \to X I N \subseteq ℝ$

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	1 2	dya2iocival	$⊢ (N \in ℤ \land X \in ℤ) \to X I N = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$
4		simpr	$⊢ (N \in ℤ \land X \in ℤ) \to X \in ℤ$
5	4	zred	$⊢ (N \in ℤ \land X \in ℤ) \to X \in ℝ$
6		2rp	$⊢ 2 \in ℝ^{+}$
7	6	a1i	$⊢ (N \in ℤ \land X \in ℤ) \to 2 \in ℝ^{+}$
8		simpl	$⊢ (N \in ℤ \land X \in ℤ) \to N \in ℤ$
9	7 8	rpexpcld	$⊢ (N \in ℤ \land X \in ℤ) \to 2^{N} \in ℝ^{+}$
10	5 9	rerpdivcld	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X}{2^{N}} \in ℝ$
11		1red	$⊢ (N \in ℤ \land X \in ℤ) \to 1 \in ℝ$
12	5 11	readdcld	$⊢ (N \in ℤ \land X \in ℤ) \to X + 1 \in ℝ$
13	12 9	rerpdivcld	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X + 1}{2^{N}} \in ℝ$
14	13	rexrd	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X + 1}{2^{N}} \in ℝ^{*}$
15		icossre	$⊢ (\frac{X}{2^{N}} \in ℝ \land \frac{X + 1}{2^{N}} \in ℝ^{*}) \to [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}}) \subseteq ℝ$
16	10 14 15	syl2anc	$⊢ (N \in ℤ \land X \in ℤ) \to [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}}) \subseteq ℝ$
17	3 16	eqsstrd	$⊢ (N \in ℤ \land X \in ℤ) \to X I N \subseteq ℝ$

Metamath Proof Explorer