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 e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
Assertion dya2iocress 
|- ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) C_ RR )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 dya2ioc.1 
 |-  I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
3 1 2 dya2iocival 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )
4 simpr 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> X e. ZZ )
5 4 zred 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> X e. RR )
6 2rp 
 |-  2 e. RR+
7 6 a1i 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> 2 e. RR+ )
8 simpl 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> N e. ZZ )
9 7 8 rpexpcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( 2 ^ N ) e. RR+ )
10 5 9 rerpdivcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X / ( 2 ^ N ) ) e. RR )
11 1red 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> 1 e. RR )
12 5 11 readdcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X + 1 ) e. RR )
13 12 9 rerpdivcld 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( X + 1 ) / ( 2 ^ N ) ) e. RR )
14 13 rexrd 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( X + 1 ) / ( 2 ^ N ) ) e. RR* )
15 icossre 
 |-  ( ( ( X / ( 2 ^ N ) ) e. RR /\ ( ( X + 1 ) / ( 2 ^ N ) ) e. RR* ) -> ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) C_ RR )
16 10 14 15 syl2anc 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) C_ RR )
17 3 16 eqsstrd 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) C_ RR )