Metamath Proof Explorer

Theorem dyaddisjlem

Description: Lemma for dyaddisj . (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 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 ) ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 simplll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. ZZ )
3 simplrl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C e. NN0 )
4 1 dyadval 
 |-  ( ( A e. ZZ /\ C e. NN0 ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
5 2 3 4 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
6 5 fveq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( A F C ) ) = ( (,) ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
7 df-ov 
 |-  ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( (,) ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
8 6 7 eqtr4di 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) )
9 simpllr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> B e. ZZ )
10 simplrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> D e. NN0 )
11 1 dyadval 
 |-  ( ( B e. ZZ /\ D e. NN0 ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
12 9 10 11 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
13 12 fveq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( B F D ) ) = ( (,) ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
14 df-ov 
 |-  ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( (,) ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
15 13 14 eqtr4di 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) )
16 8 15 ineq12d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) )
17 incom 
 |-  ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) )
18 16 17 eqtrdi 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) )
19 18 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) )
20 2 zred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. RR )
21 20 recnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. CC )
22 2nn 
 |-  2 e. NN
23 nnexpcl 
 |-  ( ( 2 e. NN /\ C e. NN0 ) -> ( 2 ^ C ) e. NN )
24 22 3 23 sylancr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) e. NN )
25 24 nncnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) e. CC )
26 nnexpcl 
 |-  ( ( 2 e. NN /\ D e. NN0 ) -> ( 2 ^ D ) e. NN )
27 22 10 26 sylancr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. NN )
28 27 nncnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. CC )
29 24 nnne0d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) =/= 0 )
30 21 25 28 29 div13d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) = ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. A ) )
31 2cnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 2 e. CC )
32 2ne0 
 |-  2 =/= 0
33 32 a1i 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 2 =/= 0 )
34 3 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C e. ZZ )
35 10 nn0zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> D e. ZZ )
36 31 33 34 35 expsubd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ ( D - C ) ) = ( ( 2 ^ D ) / ( 2 ^ C ) ) )
37 2z 
 |-  2 e. ZZ
38 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C <_ D )
39 znn0sub 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C <_ D <-> ( D - C ) e. NN0 ) )
40 34 35 39 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( C <_ D <-> ( D - C ) e. NN0 ) )
41 38 40 mpbid 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( D - C ) e. NN0 )
42 zexpcl 
 |-  ( ( 2 e. ZZ /\ ( D - C ) e. NN0 ) -> ( 2 ^ ( D - C ) ) e. ZZ )
43 37 41 42 sylancr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ ( D - C ) ) e. ZZ )
44 36 43 eqeltrrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( 2 ^ D ) / ( 2 ^ C ) ) e. ZZ )
45 44 2 zmulcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. A ) e. ZZ )
46 30 45 eqeltrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ )
47 zltp1le 
 |-  ( ( B e. ZZ /\ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ ) -> ( B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
48 9 46 47 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
49 9 zred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> B e. RR )
50 20 24 nndivred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A / ( 2 ^ C ) ) e. RR )
51 27 nnred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. RR )
52 27 nngt0d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 0 < ( 2 ^ D ) )
53 ltdivmul2 
 |-  ( ( B e. RR /\ ( A / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
54 49 50 51 52 53 syl112anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
55 peano2re 
 |-  ( B e. RR -> ( B + 1 ) e. RR )
56 49 55 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B + 1 ) e. RR )
57 ledivmul2 
 |-  ( ( ( B + 1 ) e. RR /\ ( A / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
58 56 50 51 52 57 syl112anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
59 48 54 58 3bitr4d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) ) )
60 49 27 nndivred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B / ( 2 ^ D ) ) e. RR )
61 60 rexrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B / ( 2 ^ D ) ) e. RR* )
62 56 27 nndivred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR )
63 62 rexrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* )
64 50 rexrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A / ( 2 ^ C ) ) e. RR* )
65 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
66 20 65 syl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. RR )
67 66 24 nndivred 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
68 67 rexrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* )
69 ioodisj 
 |-  ( ( ( ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) /\ ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) ) /\ ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) )
70 69 ex 
 |-  ( ( ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) /\ ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
71 61 63 64 68 70 syl22anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
72 59 71 sylbid 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
73 72 imp 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) )
74 19 73 eqtrd 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) )
75 74 3mix3d 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
76 50 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( A / ( 2 ^ C ) ) e. RR )
77 67 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
78 simprl 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) )
79 66 recnd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. CC )
80 79 25 28 29 div13d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) = ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. ( A + 1 ) ) )
81 2 peano2zd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. ZZ )
82 44 81 zmulcld 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. ( A + 1 ) ) e. ZZ )
83 80 82 eqeltrd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ )
84 zltp1le 
 |-  ( ( B e. ZZ /\ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ ) -> ( B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
85 9 83 84 syl2anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
86 ltdivmul2 
 |-  ( ( B e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
87 49 67 51 52 86 syl112anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
88 ledivmul2 
 |-  ( ( ( B + 1 ) e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
89 56 67 51 52 88 syl112anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
90 85 87 89 3bitr4d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) )
91 90 biimpa 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
92 91 adantrl 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
93 iccss 
 |-  ( ( ( ( A / ( 2 ^ C ) ) e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
94 76 77 78 92 93 syl22anc 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
95 12 fveq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( B F D ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
96 df-ov 
 |-  ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
97 95 96 eqtr4di 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
98 97 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
99 5 fveq2d 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( A F C ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
100 df-ov 
 |-  ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
101 99 100 eqtr4di 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
102 101 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
103 94 98 102 3sstr4d 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) )
104 103 3mix2d 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
105 104 anassrs 
 |-  ( ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
106 16 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) )
107 ioodisj 
 |-  ( ( ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) /\ ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) )
108 107 ex 
 |-  ( ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) /\ ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) ) )
109 64 68 61 63 108 syl22anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) ) )
110 109 imp 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) )
111 106 110 eqtrd 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) )
112 111 3mix3d 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
113 112 adantlr 
 |-  ( ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
114 60 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( B / ( 2 ^ D ) ) e. RR )
115 67 adantr 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
116 105 113 114 115 ltlecasei 
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
117 75 116 60 50 ltlecasei 
 |-  ( ( ( ( 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 ) ) ) = (/) ) )