Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Abstract measure
Borel Algebra on ` ( RR X. RR ) `
dya2iocress
Next ⟩
dya2iocbrsiga
Metamath Proof Explorer
Ascii
Unicode
Theorem
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
∈
ℤ
,
n
∈
ℤ
⟼
x
2
n
x
+
1
2
n
Assertion
dya2iocress
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
I
N
⊆
ℝ
Proof
Step
Hyp
Ref
Expression
1
sxbrsiga.0
⊢
J
=
topGen
⁡
ran
⁡
.
2
dya2ioc.1
⊢
I
=
x
∈
ℤ
,
n
∈
ℤ
⟼
x
2
n
x
+
1
2
n
3
1
2
dya2iocival
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
I
N
=
X
2
N
X
+
1
2
N
4
simpr
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
∈
ℤ
5
4
zred
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
∈
ℝ
6
2rp
⊢
2
∈
ℝ
+
7
6
a1i
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
2
∈
ℝ
+
8
simpl
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
N
∈
ℤ
9
7
8
rpexpcld
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
2
N
∈
ℝ
+
10
5
9
rerpdivcld
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
2
N
∈
ℝ
11
1red
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
1
∈
ℝ
12
5
11
readdcld
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
+
1
∈
ℝ
13
12
9
rerpdivcld
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
+
1
2
N
∈
ℝ
14
13
rexrd
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
+
1
2
N
∈
ℝ
*
15
icossre
⊢
X
2
N
∈
ℝ
∧
X
+
1
2
N
∈
ℝ
*
→
X
2
N
X
+
1
2
N
⊆
ℝ
16
10
14
15
syl2anc
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
2
N
X
+
1
2
N
⊆
ℝ
17
3
16
eqsstrd
⊢
N
∈
ℤ
∧
X
∈
ℤ
→
X
I
N
⊆
ℝ