Theorem 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=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	dya2ioc.1	$$⊢I=\left(x\in \mathbb{Z},n\in \mathbb{Z}⟼\left[\frac{x}{2^n},\frac{x+1}{2^n}\right)\right)$$
Assertion	dya2iocival	$$⊢\left(N\in \mathbb{Z}\wedge X\in \mathbb{Z}\right)\to XIN=\left[\frac{X}{2^N},\frac{X+1}{2^N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		dya2ioc.1	$$⊢I=\left(x\in \mathbb{Z},n\in \mathbb{Z}⟼\left[\frac{x}{2^n},\frac{x+1}{2^n}\right)\right)$$
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 \left[\frac{u}{2^m},\frac{u+1}{2^m}\right)=\left[\frac{X}{2^m},\frac{X+1}{2^m}\right)$$
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 \left[\frac{X}{2^m},\frac{X+1}{2^m}\right)=\left[\frac{X}{2^N},\frac{X+1}{2^N}\right)$$
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 \left[\frac{u}{2^m},\frac{u+1}{2^m}\right)=\left[\frac{x}{2^m},\frac{x+1}{2^m}\right)$$
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 \left[\frac{x}{2^m},\frac{x+1}{2^m}\right)=\left[\frac{x}{2^n},\frac{x+1}{2^n}\right)$$
19	14 18	cbvmpov	$$⊢\left(u\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{u}{2^m},\frac{u+1}{2^m}\right)\right)=\left(x\in \mathbb{Z},n\in \mathbb{Z}⟼\left[\frac{x}{2^n},\frac{x+1}{2^n}\right)\right)$$
20	2 19	eqtr4i	$$⊢I=\left(u\in \mathbb{Z},m\in \mathbb{Z}⟼\left[\frac{u}{2^m},\frac{u+1}{2^m}\right)\right)$$
21		ovex	$$⊢\left[\frac{X}{2^N},\frac{X+1}{2^N}\right)\in \mathrm{V}$$
22	6 10 20 21	ovmpo	$$⊢\left(X\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to XIN=\left[\frac{X}{2^N},\frac{X+1}{2^N}\right)$$
23	22	ancoms	$$⊢\left(N\in \mathbb{Z}\wedge X\in \mathbb{Z}\right)\to XIN=\left[\frac{X}{2^N},\frac{X+1}{2^N}\right)$$