dya2iocival

Description: The function I returns closed-below open-above dyadic rational intervals covering the real line. This is the same construction as in dyadmbl . (Contributed by Thierry Arnoux, 24-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	dya2iocival	$⊢ (N \in ℤ \land X \in ℤ) \to X I N = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$

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		oveq1	$⊢ u = X \to \frac{u}{2^{m}} = \frac{X}{2^{m}}$
4		oveq1	$⊢ u = X \to u + 1 = X + 1$
5	4	oveq1d	$⊢ u = X \to \frac{u + 1}{2^{m}} = \frac{X + 1}{2^{m}}$
6	3 5	oveq12d	$⊢ u = X \to [\frac{u}{2^{m}}, \frac{u + 1}{2^{m}}) = [\frac{X}{2^{m}}, \frac{X + 1}{2^{m}})$
7		oveq2	$⊢ m = N \to 2^{m} = 2^{N}$
8	7	oveq2d	$⊢ m = N \to \frac{X}{2^{m}} = \frac{X}{2^{N}}$
9	7	oveq2d	$⊢ m = N \to \frac{X + 1}{2^{m}} = \frac{X + 1}{2^{N}}$
10	8 9	oveq12d	$⊢ m = N \to [\frac{X}{2^{m}}, \frac{X + 1}{2^{m}}) = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$
11		oveq1	$⊢ u = x \to \frac{u}{2^{m}} = \frac{x}{2^{m}}$
12		oveq1	$⊢ u = x \to u + 1 = x + 1$
13	12	oveq1d	$⊢ u = x \to \frac{u + 1}{2^{m}} = \frac{x + 1}{2^{m}}$
14	11 13	oveq12d	$⊢ u = x \to [\frac{u}{2^{m}}, \frac{u + 1}{2^{m}}) = [\frac{x}{2^{m}}, \frac{x + 1}{2^{m}})$
15		oveq2	$⊢ m = n \to 2^{m} = 2^{n}$
16	15	oveq2d	$⊢ m = n \to \frac{x}{2^{m}} = \frac{x}{2^{n}}$
17	15	oveq2d	$⊢ m = n \to \frac{x + 1}{2^{m}} = \frac{x + 1}{2^{n}}$
18	16 17	oveq12d	$⊢ m = n \to [\frac{x}{2^{m}}, \frac{x + 1}{2^{m}}) = [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}})$
19	14 18	cbvmpov	$⊢ (u \in ℤ, m \in ℤ ⟼ [\frac{u}{2^{m}}, \frac{u + 1}{2^{m}})) = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
20	2 19	eqtr4i	$⊢ I = (u \in ℤ, m \in ℤ ⟼ [\frac{u}{2^{m}}, \frac{u + 1}{2^{m}}))$
21		ovex	$⊢ [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}}) \in V$
22	6 10 20 21	ovmpo	$⊢ (X \in ℤ \land N \in ℤ) \to X I N = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$
23	22	ancoms	$⊢ (N \in ℤ \land X \in ℤ) \to X I N = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$

Metamath Proof Explorer

Theorem dya2iocival

Proof