Metamath Proof Explorer

Theorem dyaddisj

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)

Ref Expression
Hypothesis dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
Assertion dyaddisj 
|- ( ( A e. ran F /\ B e. ran F ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` 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 dyadf 
 |-  F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
3 ffn 
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> F Fn ( ZZ X. NN0 ) )
4 ovelrn 
 |-  ( F Fn ( ZZ X. NN0 ) -> ( A e. ran F <-> E. a e. ZZ E. c e. NN0 A = ( a F c ) ) )
5 ovelrn 
 |-  ( F Fn ( ZZ X. NN0 ) -> ( B e. ran F <-> E. b e. ZZ E. d e. NN0 B = ( b F d ) ) )
6 4 5 anbi12d 
 |-  ( F Fn ( ZZ X. NN0 ) -> ( ( A e. ran F /\ B e. ran F ) <-> ( E. a e. ZZ E. c e. NN0 A = ( a F c ) /\ E. b e. ZZ E. d e. NN0 B = ( b F d ) ) ) )
7 2 3 6 mp2b 
 |-  ( ( A e. ran F /\ B e. ran F ) <-> ( E. a e. ZZ E. c e. NN0 A = ( a F c ) /\ E. b e. ZZ E. d e. NN0 B = ( b F d ) ) )
8 reeanv 
 |-  ( E. a e. ZZ E. b e. ZZ ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) <-> ( E. a e. ZZ E. c e. NN0 A = ( a F c ) /\ E. b e. ZZ E. d e. NN0 B = ( b F d ) ) )
9 7 8 bitr4i 
 |-  ( ( A e. ran F /\ B e. ran F ) <-> E. a e. ZZ E. b e. ZZ ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) )
10 reeanv 
 |-  ( E. c e. NN0 E. d e. NN0 ( A = ( a F c ) /\ B = ( b F d ) ) <-> ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) )
11 nn0re 
 |-  ( c e. NN0 -> c e. RR )
12 11 ad2antrl 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> c e. RR )
13 nn0re 
 |-  ( d e. NN0 -> d e. RR )
14 13 ad2antll 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> d e. RR )
15 1 dyaddisjlem 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) /\ c <_ d ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
16 ancom 
 |-  ( ( a e. ZZ /\ b e. ZZ ) <-> ( b e. ZZ /\ a e. ZZ ) )
17 ancom 
 |-  ( ( c e. NN0 /\ d e. NN0 ) <-> ( d e. NN0 /\ c e. NN0 ) )
18 16 17 anbi12i 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) <-> ( ( b e. ZZ /\ a e. ZZ ) /\ ( d e. NN0 /\ c e. NN0 ) ) )
19 1 dyaddisjlem 
 |-  ( ( ( ( b e. ZZ /\ a e. ZZ ) /\ ( d e. NN0 /\ c e. NN0 ) ) /\ d <_ c ) -> ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) )
20 18 19 sylanb 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) /\ d <_ c ) -> ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) )
21 orcom 
 |-  ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) )
22 incom 
 |-  ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) )
23 22 eqeq1i 
 |-  ( ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) <-> ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) )
24 21 23 orbi12i 
 |-  ( ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) <-> ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
25 df-3or 
 |-  ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) <-> ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) )
26 df-3or 
 |-  ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) <-> ( ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
27 24 25 26 3bitr4i 
 |-  ( ( ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( ( (,) ` ( b F d ) ) i^i ( (,) ` ( a F c ) ) ) = (/) ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
28 20 27 sylib 
 |-  ( ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) /\ d <_ c ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
29 12 14 15 28 lecasei 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
30 simpl 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> A = ( a F c ) )
31 30 fveq2d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( [,] ` A ) = ( [,] ` ( a F c ) ) )
32 simpr 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> B = ( b F d ) )
33 32 fveq2d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( [,] ` B ) = ( [,] ` ( b F d ) ) )
34 31 33 sseq12d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) <-> ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) ) )
35 33 31 sseq12d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` B ) C_ ( [,] ` A ) <-> ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) ) )
36 30 fveq2d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( (,) ` A ) = ( (,) ` ( a F c ) ) )
37 32 fveq2d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( (,) ` B ) = ( (,) ` ( b F d ) ) )
38 36 37 ineq12d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( (,) ` A ) i^i ( (,) ` B ) ) = ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) )
39 38 eqeq1d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) <-> ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) )
40 34 35 39 3orbi123d 
 |-  ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) <-> ( ( [,] ` ( a F c ) ) C_ ( [,] ` ( b F d ) ) \/ ( [,] ` ( b F d ) ) C_ ( [,] ` ( a F c ) ) \/ ( ( (,) ` ( a F c ) ) i^i ( (,) ` ( b F d ) ) ) = (/) ) ) )
41 29 40 syl5ibrcom 
 |-  ( ( ( a e. ZZ /\ b e. ZZ ) /\ ( c e. NN0 /\ d e. NN0 ) ) -> ( ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) )
42 41 rexlimdvva 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( E. c e. NN0 E. d e. NN0 ( A = ( a F c ) /\ B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) )
43 10 42 biimtrrid 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) ) )
44 43 rexlimivv 
 |-  ( E. a e. ZZ E. b e. ZZ ( E. c e. NN0 A = ( a F c ) /\ E. d e. NN0 B = ( b F d ) ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) )
45 9 44 sylbi 
 |-  ( ( A e. ran F /\ B e. ran F ) -> ( ( [,] ` A ) C_ ( [,] ` B ) \/ ( [,] ` B ) C_ ( [,] ` A ) \/ ( ( (,) ` A ) i^i ( (,) ` B ) ) = (/) ) )