dya2iocbrsiga

Description: Dyadic intervals are Borel sets of RR . (Contributed by Thierry Arnoux, 22-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	dya2iocbrsiga	$⊢ (N \in ℤ \land X \in ℤ) \to X I N \in 𝔅_{ℝ}$

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	1 2	dya2iocival	$⊢ (N \in ℤ \land X \in ℤ) \to X I N = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$
4		mnfxr	$⊢ −∞ \in ℝ^{*}$
5	4	a1i	$⊢ (N \in ℤ \land X \in ℤ) \to −∞ \in ℝ^{*}$
6		simpr	$⊢ (N \in ℤ \land X \in ℤ) \to X \in ℤ$
7	6	zred	$⊢ (N \in ℤ \land X \in ℤ) \to X \in ℝ$
8		2rp	$⊢ 2 \in ℝ^{+}$
9	8	a1i	$⊢ (N \in ℤ \land X \in ℤ) \to 2 \in ℝ^{+}$
10		simpl	$⊢ (N \in ℤ \land X \in ℤ) \to N \in ℤ$
11	9 10	rpexpcld	$⊢ (N \in ℤ \land X \in ℤ) \to 2^{N} \in ℝ^{+}$
12	7 11	rerpdivcld	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X}{2^{N}} \in ℝ$
13	12	rexrd	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X}{2^{N}} \in ℝ^{*}$
14		1red	$⊢ (N \in ℤ \land X \in ℤ) \to 1 \in ℝ$
15	7 14	readdcld	$⊢ (N \in ℤ \land X \in ℤ) \to X + 1 \in ℝ$
16	15 11	rerpdivcld	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X + 1}{2^{N}} \in ℝ$
17	16	rexrd	$⊢ (N \in ℤ \land X \in ℤ) \to \frac{X + 1}{2^{N}} \in ℝ^{*}$
18		mnflt	$⊢ \frac{X}{2^{N}} \in ℝ \to −∞ < \frac{X}{2^{N}}$
19	12 18	syl	$⊢ (N \in ℤ \land X \in ℤ) \to −∞ < \frac{X}{2^{N}}$
20		difioo	$⊢ ((−∞ \in ℝ^{} \land \frac{X}{2^{N}} \in ℝ^{} \land \frac{X + 1}{2^{N}} \in ℝ^{*}) \land −∞ < \frac{X}{2^{N}}) \to (−∞, \frac{X + 1}{2^{N}}) ∖ (−∞, \frac{X}{2^{N}}) = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$
21	5 13 17 19 20	syl31anc	$⊢ (N \in ℤ \land X \in ℤ) \to (−∞, \frac{X + 1}{2^{N}}) ∖ (−∞, \frac{X}{2^{N}}) = [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}})$
22		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
23		elrnsiga	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
24	22 23	ax-mp	$⊢ 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
25		retop	$⊢ topGen (ran (.)) \in Top$
26		iooretop	$⊢ (−∞, \frac{X + 1}{2^{N}}) \in topGen (ran (.))$
27		elsigagen	$⊢ (topGen (ran (.)) \in Top \land (−∞, \frac{X + 1}{2^{N}}) \in topGen (ran (.))) \to (−∞, \frac{X + 1}{2^{N}}) \in 𝛔 (topGen (ran (.)))$
28	25 26 27	mp2an	$⊢ (−∞, \frac{X + 1}{2^{N}}) \in 𝛔 (topGen (ran (.)))$
29		df-brsiga	$⊢ 𝔅_{ℝ} = 𝛔 (topGen (ran (.)))$
30	28 29	eleqtrri	$⊢ (−∞, \frac{X + 1}{2^{N}}) \in 𝔅_{ℝ}$
31		iooretop	$⊢ (−∞, \frac{X}{2^{N}}) \in topGen (ran (.))$
32		elsigagen	$⊢ (topGen (ran (.)) \in Top \land (−∞, \frac{X}{2^{N}}) \in topGen (ran (.))) \to (−∞, \frac{X}{2^{N}}) \in 𝛔 (topGen (ran (.)))$
33	25 31 32	mp2an	$⊢ (−∞, \frac{X}{2^{N}}) \in 𝛔 (topGen (ran (.)))$
34	33 29	eleqtrri	$⊢ (−∞, \frac{X}{2^{N}}) \in 𝔅_{ℝ}$
35		difelsiga	$⊢ (𝔅_{ℝ} \in ⋃ ran sigAlgebra \land (−∞, \frac{X + 1}{2^{N}}) \in 𝔅_{ℝ} \land (−∞, \frac{X}{2^{N}}) \in 𝔅_{ℝ}) \to (−∞, \frac{X + 1}{2^{N}}) ∖ (−∞, \frac{X}{2^{N}}) \in 𝔅_{ℝ}$
36	24 30 34 35	mp3an	$⊢ (−∞, \frac{X + 1}{2^{N}}) ∖ (−∞, \frac{X}{2^{N}}) \in 𝔅_{ℝ}$
37	21 36	eqeltrrdi	$⊢ (N \in ℤ \land X \in ℤ) \to [\frac{X}{2^{N}}, \frac{X + 1}{2^{N}}) \in 𝔅_{ℝ}$
38	3 37	eqeltrd	$⊢ (N \in ℤ \land X \in ℤ) \to X I N \in 𝔅_{ℝ}$

Metamath Proof Explorer

Theorem dya2iocbrsiga

Proof