Metamath Proof Explorer

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 = ( topGen ` ran (,) )
dya2ioc.1 
|- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
Assertion dya2iocival 
|- ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )

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 oveq1 
 |-  ( u = X -> ( u / ( 2 ^ m ) ) = ( X / ( 2 ^ m ) ) )
4 oveq1 
 |-  ( u = X -> ( u + 1 ) = ( X + 1 ) )
5 4 oveq1d 
 |-  ( u = X -> ( ( u + 1 ) / ( 2 ^ m ) ) = ( ( X + 1 ) / ( 2 ^ m ) ) )
6 3 5 oveq12d 
 |-  ( u = X -> ( ( u / ( 2 ^ m ) ) [,) ( ( u + 1 ) / ( 2 ^ m ) ) ) = ( ( X / ( 2 ^ m ) ) [,) ( ( X + 1 ) / ( 2 ^ m ) ) ) )
7 oveq2 
 |-  ( m = N -> ( 2 ^ m ) = ( 2 ^ N ) )
8 7 oveq2d 
 |-  ( m = N -> ( X / ( 2 ^ m ) ) = ( X / ( 2 ^ N ) ) )
9 7 oveq2d 
 |-  ( m = N -> ( ( X + 1 ) / ( 2 ^ m ) ) = ( ( X + 1 ) / ( 2 ^ N ) ) )
10 8 9 oveq12d 
 |-  ( m = N -> ( ( X / ( 2 ^ m ) ) [,) ( ( X + 1 ) / ( 2 ^ m ) ) ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )
11 oveq1 
 |-  ( u = x -> ( u / ( 2 ^ m ) ) = ( x / ( 2 ^ m ) ) )
12 oveq1 
 |-  ( u = x -> ( u + 1 ) = ( x + 1 ) )
13 12 oveq1d 
 |-  ( u = x -> ( ( u + 1 ) / ( 2 ^ m ) ) = ( ( x + 1 ) / ( 2 ^ m ) ) )
14 11 13 oveq12d 
 |-  ( u = x -> ( ( u / ( 2 ^ m ) ) [,) ( ( u + 1 ) / ( 2 ^ m ) ) ) = ( ( x / ( 2 ^ m ) ) [,) ( ( x + 1 ) / ( 2 ^ m ) ) ) )
15 oveq2 
 |-  ( m = n -> ( 2 ^ m ) = ( 2 ^ n ) )
16 15 oveq2d 
 |-  ( m = n -> ( x / ( 2 ^ m ) ) = ( x / ( 2 ^ n ) ) )
17 15 oveq2d 
 |-  ( m = n -> ( ( x + 1 ) / ( 2 ^ m ) ) = ( ( x + 1 ) / ( 2 ^ n ) ) )
18 16 17 oveq12d 
 |-  ( m = n -> ( ( x / ( 2 ^ m ) ) [,) ( ( x + 1 ) / ( 2 ^ m ) ) ) = ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
19 14 18 cbvmpov 
 |-  ( u e. ZZ , m e. ZZ |-> ( ( u / ( 2 ^ m ) ) [,) ( ( u + 1 ) / ( 2 ^ m ) ) ) ) = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
20 2 19 eqtr4i 
 |-  I = ( u e. ZZ , m e. ZZ |-> ( ( u / ( 2 ^ m ) ) [,) ( ( u + 1 ) / ( 2 ^ m ) ) ) )
21 ovex 
 |-  ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) e. _V
22 6 10 20 21 ovmpo 
 |-  ( ( X e. ZZ /\ N e. ZZ ) -> ( X I N ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )
23 22 ancoms 
 |-  ( ( N e. ZZ /\ X e. ZZ ) -> ( X I N ) = ( ( X / ( 2 ^ N ) ) [,) ( ( X + 1 ) / ( 2 ^ N ) ) ) )