This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dyadss

Description: Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015) (Proof shortened by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypothesis dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
Assertion dyadss 
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) -> D <_ C ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) )
3 simpllr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> B e. ZZ )
4 simplrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> D e. NN0 )
5 1 dyadval 
 |-  ( ( B e. ZZ /\ D e. NN0 ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
6 3 4 5 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
7 6 fveq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( [,] ` ( B F D ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
8 df-ov 
 |-  ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
9 7 8 eqtr4di 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
10 3 zred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> B e. RR )
11 2nn 
 |-  2 e. NN
12 nnexpcl 
 |-  ( ( 2 e. NN /\ D e. NN0 ) -> ( 2 ^ D ) e. NN )
13 11 4 12 sylancr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( 2 ^ D ) e. NN )
14 10 13 nndivred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( B / ( 2 ^ D ) ) e. RR )
15 peano2re 
 |-  ( B e. RR -> ( B + 1 ) e. RR )
16 10 15 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( B + 1 ) e. RR )
17 16 13 nndivred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR )
18 iccssre 
 |-  ( ( ( B / ( 2 ^ D ) ) e. RR /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ RR )
19 14 17 18 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ RR )
20 9 19 eqsstrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( [,] ` ( B F D ) ) C_ RR )
21 ovolss 
 |-  ( ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) /\ ( [,] ` ( B F D ) ) C_ RR ) -> ( vol* ` ( [,] ` ( A F C ) ) ) <_ ( vol* ` ( [,] ` ( B F D ) ) ) )
22 2 20 21 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( vol* ` ( [,] ` ( A F C ) ) ) <_ ( vol* ` ( [,] ` ( B F D ) ) ) )
23 simplll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> A e. ZZ )
24 simplrl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> C e. NN0 )
25 1 dyadovol 
 |-  ( ( A e. ZZ /\ C e. NN0 ) -> ( vol* ` ( [,] ` ( A F C ) ) ) = ( 1 / ( 2 ^ C ) ) )
26 23 24 25 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( vol* ` ( [,] ` ( A F C ) ) ) = ( 1 / ( 2 ^ C ) ) )
27 1 dyadovol 
 |-  ( ( B e. ZZ /\ D e. NN0 ) -> ( vol* ` ( [,] ` ( B F D ) ) ) = ( 1 / ( 2 ^ D ) ) )
28 3 4 27 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( vol* ` ( [,] ` ( B F D ) ) ) = ( 1 / ( 2 ^ D ) ) )
29 22 26 28 3brtr3d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( 1 / ( 2 ^ C ) ) <_ ( 1 / ( 2 ^ D ) ) )
30 nnexpcl 
 |-  ( ( 2 e. NN /\ C e. NN0 ) -> ( 2 ^ C ) e. NN )
31 11 24 30 sylancr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( 2 ^ C ) e. NN )
32 nnre 
 |-  ( ( 2 ^ D ) e. NN -> ( 2 ^ D ) e. RR )
33 nngt0 
 |-  ( ( 2 ^ D ) e. NN -> 0 < ( 2 ^ D ) )
34 32 33 jca 
 |-  ( ( 2 ^ D ) e. NN -> ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) )
35 nnre 
 |-  ( ( 2 ^ C ) e. NN -> ( 2 ^ C ) e. RR )
36 nngt0 
 |-  ( ( 2 ^ C ) e. NN -> 0 < ( 2 ^ C ) )
37 35 36 jca 
 |-  ( ( 2 ^ C ) e. NN -> ( ( 2 ^ C ) e. RR /\ 0 < ( 2 ^ C ) ) )
38 lerec 
 |-  ( ( ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) /\ ( ( 2 ^ C ) e. RR /\ 0 < ( 2 ^ C ) ) ) -> ( ( 2 ^ D ) <_ ( 2 ^ C ) <-> ( 1 / ( 2 ^ C ) ) <_ ( 1 / ( 2 ^ D ) ) ) )
39 34 37 38 syl2an 
 |-  ( ( ( 2 ^ D ) e. NN /\ ( 2 ^ C ) e. NN ) -> ( ( 2 ^ D ) <_ ( 2 ^ C ) <-> ( 1 / ( 2 ^ C ) ) <_ ( 1 / ( 2 ^ D ) ) ) )
40 13 31 39 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( ( 2 ^ D ) <_ ( 2 ^ C ) <-> ( 1 / ( 2 ^ C ) ) <_ ( 1 / ( 2 ^ D ) ) ) )
41 29 40 mpbird 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( 2 ^ D ) <_ ( 2 ^ C ) )
42 2re 
 |-  2 e. RR
43 42 a1i 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> 2 e. RR )
44 4 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> D e. ZZ )
45 24 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> C e. ZZ )
46 1lt2 
 |-  1 < 2
47 46 a1i 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> 1 < 2 )
48 43 44 45 47 leexp2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> ( D <_ C <-> ( 2 ^ D ) <_ ( 2 ^ C ) ) )
49 41 48 mpbird 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) ) -> D <_ C )
50 49 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) -> D <_ C ) )