Metamath Proof Explorer


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