Metamath Proof Explorer

Theorem dyadval

Description: Value of the dyadic rational function F . (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 dyadval 
|- ( ( A e. ZZ /\ B e. NN0 ) -> ( A F B ) = <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 id 
 |-  ( x = A -> x = A )
3 oveq2 
 |-  ( y = B -> ( 2 ^ y ) = ( 2 ^ B ) )
4 2 3 oveqan12d 
 |-  ( ( x = A /\ y = B ) -> ( x / ( 2 ^ y ) ) = ( A / ( 2 ^ B ) ) )
5 oveq1 
 |-  ( x = A -> ( x + 1 ) = ( A + 1 ) )
6 5 3 oveqan12d 
 |-  ( ( x = A /\ y = B ) -> ( ( x + 1 ) / ( 2 ^ y ) ) = ( ( A + 1 ) / ( 2 ^ B ) ) )
7 4 6 opeq12d 
 |-  ( ( x = A /\ y = B ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. = <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. )
8 opex 
 |-  <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. e. _V
9 7 1 8 ovmpoa 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A F B ) = <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. )