Metamath Proof Explorer

Theorem dyadf

Description: The function F returns the endpoints of a dyadic rational covering of the real line. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
Assertion dyadf 
|- F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 zre 
 |-  ( x e. ZZ -> x e. RR )
3 2 adantr 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> x e. RR )
4 3 lep1d 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> x <_ ( x + 1 ) )
5 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
6 3 5 syl 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( x + 1 ) e. RR )
7 2nn 
 |-  2 e. NN
8 nnexpcl 
 |-  ( ( 2 e. NN /\ y e. NN0 ) -> ( 2 ^ y ) e. NN )
9 7 8 mpan 
 |-  ( y e. NN0 -> ( 2 ^ y ) e. NN )
10 9 adantl 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( 2 ^ y ) e. NN )
11 10 nnred 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( 2 ^ y ) e. RR )
12 10 nngt0d 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> 0 < ( 2 ^ y ) )
13 lediv1 
 |-  ( ( x e. RR /\ ( x + 1 ) e. RR /\ ( ( 2 ^ y ) e. RR /\ 0 < ( 2 ^ y ) ) ) -> ( x <_ ( x + 1 ) <-> ( x / ( 2 ^ y ) ) <_ ( ( x + 1 ) / ( 2 ^ y ) ) ) )
14 3 6 11 12 13 syl112anc 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( x <_ ( x + 1 ) <-> ( x / ( 2 ^ y ) ) <_ ( ( x + 1 ) / ( 2 ^ y ) ) ) )
15 4 14 mpbid 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( x / ( 2 ^ y ) ) <_ ( ( x + 1 ) / ( 2 ^ y ) ) )
16 df-br 
 |-  ( ( x / ( 2 ^ y ) ) <_ ( ( x + 1 ) / ( 2 ^ y ) ) <-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. <_ )
17 15 16 sylib 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. <_ )
18 nndivre 
 |-  ( ( x e. RR /\ ( 2 ^ y ) e. NN ) -> ( x / ( 2 ^ y ) ) e. RR )
19 2 9 18 syl2an 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( x / ( 2 ^ y ) ) e. RR )
20 2 5 syl 
 |-  ( x e. ZZ -> ( x + 1 ) e. RR )
21 nndivre 
 |-  ( ( ( x + 1 ) e. RR /\ ( 2 ^ y ) e. NN ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
22 20 9 21 syl2an 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
23 19 22 opelxpd 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
24 17 23 elind 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( <_ i^i ( RR X. RR ) ) )
25 24 rgen2 
 |-  A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( <_ i^i ( RR X. RR ) )
26 1 fmpo 
 |-  ( A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( <_ i^i ( RR X. RR ) ) <-> F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) )
27 25 26 mpbi 
 |-  F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )