Metamath Proof Explorer

Theorem dyadovol

Description: Volume of a dyadic rational interval. (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 dyadovol 
|- ( ( A e. ZZ /\ B e. NN0 ) -> ( vol* ` ( [,] ` ( A F B ) ) ) = ( 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 1 dyadval 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A F B ) = <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. )
3 2 fveq2d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( [,] ` ( A F B ) ) = ( [,] ` <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. ) )
4 df-ov 
 |-  ( ( A / ( 2 ^ B ) ) [,] ( ( A + 1 ) / ( 2 ^ B ) ) ) = ( [,] ` <. ( A / ( 2 ^ B ) ) , ( ( A + 1 ) / ( 2 ^ B ) ) >. )
5 3 4 eqtr4di 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( [,] ` ( A F B ) ) = ( ( A / ( 2 ^ B ) ) [,] ( ( A + 1 ) / ( 2 ^ B ) ) ) )
6 5 fveq2d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( vol* ` ( [,] ` ( A F B ) ) ) = ( vol* ` ( ( A / ( 2 ^ B ) ) [,] ( ( A + 1 ) / ( 2 ^ B ) ) ) ) )
7 zre 
 |-  ( A e. ZZ -> A e. RR )
8 2nn 
 |-  2 e. NN
9 nnexpcl 
 |-  ( ( 2 e. NN /\ B e. NN0 ) -> ( 2 ^ B ) e. NN )
10 8 9 mpan 
 |-  ( B e. NN0 -> ( 2 ^ B ) e. NN )
11 nndivre 
 |-  ( ( A e. RR /\ ( 2 ^ B ) e. NN ) -> ( A / ( 2 ^ B ) ) e. RR )
12 7 10 11 syl2an 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A / ( 2 ^ B ) ) e. RR )
13 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
14 7 13 syl 
 |-  ( A e. ZZ -> ( A + 1 ) e. RR )
15 nndivre 
 |-  ( ( ( A + 1 ) e. RR /\ ( 2 ^ B ) e. NN ) -> ( ( A + 1 ) / ( 2 ^ B ) ) e. RR )
16 14 10 15 syl2an 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( ( A + 1 ) / ( 2 ^ B ) ) e. RR )
17 7 adantr 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> A e. RR )
18 17 lep1d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> A <_ ( A + 1 ) )
19 17 13 syl 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A + 1 ) e. RR )
20 10 adantl 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( 2 ^ B ) e. NN )
21 20 nnred 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( 2 ^ B ) e. RR )
22 20 nngt0d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> 0 < ( 2 ^ B ) )
23 lediv1 
 |-  ( ( A e. RR /\ ( A + 1 ) e. RR /\ ( ( 2 ^ B ) e. RR /\ 0 < ( 2 ^ B ) ) ) -> ( A <_ ( A + 1 ) <-> ( A / ( 2 ^ B ) ) <_ ( ( A + 1 ) / ( 2 ^ B ) ) ) )
24 17 19 21 22 23 syl112anc 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A <_ ( A + 1 ) <-> ( A / ( 2 ^ B ) ) <_ ( ( A + 1 ) / ( 2 ^ B ) ) ) )
25 18 24 mpbid 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A / ( 2 ^ B ) ) <_ ( ( A + 1 ) / ( 2 ^ B ) ) )
26 ovolicc 
 |-  ( ( ( A / ( 2 ^ B ) ) e. RR /\ ( ( A + 1 ) / ( 2 ^ B ) ) e. RR /\ ( A / ( 2 ^ B ) ) <_ ( ( A + 1 ) / ( 2 ^ B ) ) ) -> ( vol* ` ( ( A / ( 2 ^ B ) ) [,] ( ( A + 1 ) / ( 2 ^ B ) ) ) ) = ( ( ( A + 1 ) / ( 2 ^ B ) ) - ( A / ( 2 ^ B ) ) ) )
27 12 16 25 26 syl3anc 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( vol* ` ( ( A / ( 2 ^ B ) ) [,] ( ( A + 1 ) / ( 2 ^ B ) ) ) ) = ( ( ( A + 1 ) / ( 2 ^ B ) ) - ( A / ( 2 ^ B ) ) ) )
28 19 recnd 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( A + 1 ) e. CC )
29 17 recnd 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> A e. CC )
30 21 recnd 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( 2 ^ B ) e. CC )
31 20 nnne0d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( 2 ^ B ) =/= 0 )
32 28 29 30 31 divsubdird 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( ( ( A + 1 ) - A ) / ( 2 ^ B ) ) = ( ( ( A + 1 ) / ( 2 ^ B ) ) - ( A / ( 2 ^ B ) ) ) )
33 ax-1cn 
 |-  1 e. CC
34 pncan2 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - A ) = 1 )
35 29 33 34 sylancl 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( ( A + 1 ) - A ) = 1 )
36 35 oveq1d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( ( ( A + 1 ) - A ) / ( 2 ^ B ) ) = ( 1 / ( 2 ^ B ) ) )
37 32 36 eqtr3d 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( ( ( A + 1 ) / ( 2 ^ B ) ) - ( A / ( 2 ^ B ) ) ) = ( 1 / ( 2 ^ B ) ) )
38 6 27 37 3eqtrd 
 |-  ( ( A e. ZZ /\ B e. NN0 ) -> ( vol* ` ( [,] ` ( A F B ) ) ) = ( 1 / ( 2 ^ B ) ) )